lean4-htt

Author SHA1 Message Date

Author	SHA1	Message	Date
Kim Morrison	40eefb1df6	feat: alignment of `List/Array/Vector` lemmas about `range`, `range'`, `zipIdx` (#6878 ) This PR completes alignments of `List/Array/Vector` lemmas about `range`, `range'`, and `zipIdx`.	2025-01-31 00:06:51 +00:00
Kim Morrison	7e8af0fc9d	feat: rename `List.enum(From)` to `List.zipIdx`, and `Array/Vector.zipWithIndex` to `zipIdx` (#6800 ) This PR uniformizes the naming of `enum`/`enumFrom` (on `List`) and `zipWithIndex` (on `Array` on `Vector`), replacing all with `zipIdx`. At the same time, we generalize to add an optional `Nat` parameter for the initial value of the index (which previously existed, only for `List`, as the separate function `enumFrom`).	2025-01-28 23:34:30 +00:00
Kim Morrison	ac6a29ee83	feat: complete alignment of `{List,Array,Vector}.{mapIdx,mapFinIdx}` (#6701 ) This PR completes aligning `mapIdx` and `mapFinIdx` across `List/Array/Vector`.	2025-01-20 04:06:37 +00:00

Kim Morrison

40eefb1df6

feat: alignment of List/Array/Vector lemmas about range, range', zipIdx (#6878 )

This PR completes alignments of `List/Array/Vector` lemmas about
`range`, `range'`, and `zipIdx`.

2025-01-31 00:06:51 +00:00

Kim Morrison

7e8af0fc9d

feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800 )

This PR uniformizes the naming of `enum`/`enumFrom` (on `List`) and
`zipWithIndex` (on `Array` on `Vector`), replacing all with `zipIdx`. At
the same time, we generalize to add an optional `Nat` parameter for the
initial value of the index (which previously existed, only for `List`,
as the separate function `enumFrom`).

2025-01-28 23:34:30 +00:00

Kim Morrison

ac6a29ee83

feat: complete alignment of {List,Array,Vector}.{mapIdx,mapFinIdx} (#6701 )

This PR completes aligning `mapIdx` and `mapFinIdx` across
`List/Array/Vector`.

2025-01-20 04:06:37 +00:00

3 commits