max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/Omega
History
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
..
Coeffs.lean feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800) 2025-01-28 23:34:30 +00:00
Constraint.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
Int.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
IntList.lean chore: cleanup of List/Array lemmas (#6249) 2024-11-29 06:12:38 +00:00
LinearCombo.lean feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800) 2025-01-28 23:34:30 +00:00
Logic.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00