Commit 2024-05-26 03:16 2aca580b

View on Github →

feat: List.iterate (#13214) This PR add an new function for list: List.iterate. iterate f a n is [a, f a, ..., f^[n - 1] a]. The name matches Haskell's iterate

Estimated changes

added def List.iterate
added def List.iterateTR
added theorem List.iterateTR_loop_eq
added theorem List.get?_iterate
added theorem List.get_iterate
added theorem List.iterate_eq_nil
added theorem List.length_iterate
added theorem List.mem_iterate
added theorem List.range_map_iterate