lean4-htt/src/Init/Data/List
Kim Morrison 1d9b19189a chore: deprecate Array.get
fix test
2025-02-19 08:48:33 +11:00
..
Nat chore: cleanup duplicate theorems (#7113) 2025-02-18 01:46:12 +00:00
Sort chore: linting variable names for List (#7107) 2025-02-17 14:50:43 +00:00
Attach.lean chore: repair defeqs for List GetElem instances (#7121) 2025-02-18 02:19:08 +00:00
Basic.lean chore: linting variable names for List (#7107) 2025-02-17 14:50:43 +00:00
BasicAux.lean chore: repair defeqs for List GetElem instances (#7121) 2025-02-18 02:19:08 +00:00
Control.lean chore: linting variable names for List (#7107) 2025-02-17 14:50:43 +00:00
Count.lean chore: linting variable names for List (#7107) 2025-02-17 14:50:43 +00:00
Erase.lean chore: linting variable names for List (#7107) 2025-02-17 14:50:43 +00:00
Find.lean chore: cleanup duplicate theorems (#7113) 2025-02-18 01:46:12 +00:00
FinRange.lean chore: linting variable names for List (#7107) 2025-02-17 14:50:43 +00:00
Impl.lean chore: cleanup duplicate theorems (#7113) 2025-02-18 01:46:12 +00:00
Lemmas.lean chore: repair defeqs for List GetElem instances (#7121) 2025-02-18 02:19:08 +00:00
Lex.lean chore: linting variable names for List (#7107) 2025-02-17 14:50:43 +00:00
MapIdx.lean chore: linting variable names for List (#7107) 2025-02-17 14:50:43 +00:00
MinMax.lean chore: linting variable names for List (#7107) 2025-02-17 14:50:43 +00:00
Monadic.lean chore: review uses of generalize (#7126) 2025-02-18 14:07:40 +00:00
Nat.lean feat: Array.swap_perm (#6272) 2024-12-01 08:35:28 +00:00
Notation.lean chore: deprecate Array.get 2025-02-19 08:48:33 +11:00
OfFn.lean chore: fix linter.listVariables naming (#7044) 2025-02-12 05:17:39 +00:00
Pairwise.lean feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
Perm.lean chore: fix linter.listVariables naming (#7044) 2025-02-12 05:17:39 +00:00
Range.lean chore: cleanup duplicate theorems (#7113) 2025-02-18 01:46:12 +00:00
Sort.lean feat: List.mergeSort (#5092) 2024-08-20 06:32:52 +00:00
Sublist.lean chore: review uses of generalize (#7126) 2025-02-18 14:07:40 +00:00
TakeDrop.lean feat: align Array/Vector.extract lemmas with List (#7105) 2025-02-17 04:56:04 +00:00
ToArray.lean chore: use as[i] instead of as.get i 2025-02-19 08:48:33 +11:00
ToArrayImpl.lean chore: fix linter.listVariables naming (#7044) 2025-02-12 05:17:39 +00:00
Zip.lean chore: fix linter.listVariables naming (#7044) 2025-02-12 05:17:39 +00:00