| .. |
|
Lex
|
chore: cleanup simp lemmas, following the simpNF linter (#8481)
|
2025-05-26 04:13:17 +00:00 |
|
QSort
|
feat: verification of qsort via grind (#7995)
|
2025-05-24 04:01:55 +00:00 |
|
Subarray
|
feat: do not export def bodies by default (#8221)
|
2025-05-15 12:16:54 +00:00 |
|
Attach.lean
|
refactor: Init: expose lots of functions (#8501)
|
2025-05-28 07:37:54 +00:00 |
|
Basic.lean
|
fix: make Array.size not reducible (#8513)
|
2025-05-28 12:37:24 +00:00 |
|
BasicAux.lean
|
fix: replace bad simp lemmas for Id (#7352)
|
2025-05-22 22:45:35 +00:00 |
|
BinSearch.lean
|
fix: replace bad simp lemmas for Id (#7352)
|
2025-05-22 22:45:35 +00:00 |
|
Bootstrap.lean
|
fix: make Array.size not reducible (#8513)
|
2025-05-28 12:37:24 +00:00 |
|
Count.lean
|
fix: make Array.size not reducible (#8513)
|
2025-05-28 12:37:24 +00:00 |
|
DecidableEq.lean
|
fix: make Array.size not reducible (#8513)
|
2025-05-28 12:37:24 +00:00 |
|
Erase.lean
|
chore: cleanup simp lemmas, following the simpNF linter (#8481)
|
2025-05-26 04:13:17 +00:00 |
|
Extract.lean
|
chore: cleanup simp lemmas, following the simpNF linter (#8481)
|
2025-05-26 04:13:17 +00:00 |
|
Find.lean
|
fix: make Array.size not reducible (#8513)
|
2025-05-28 12:37:24 +00:00 |
|
FinRange.lean
|
feat: enable experimental module system in Init (#8047)
|
2025-04-23 17:21:33 +00:00 |
|
GetLit.lean
|
feat: do not export def bodies by default (#8221)
|
2025-05-15 12:16:54 +00:00 |
|
InsertIdx.lean
|
fix: make Array.size not reducible (#8513)
|
2025-05-28 12:37:24 +00:00 |
|
InsertionSort.lean
|
feat: enable experimental module system in Init (#8047)
|
2025-04-23 17:21:33 +00:00 |
|
Lemmas.lean
|
chore: initial @[grind] annotations for Array/Vector.range (#8606)
|
2025-06-03 06:44:01 +00:00 |
|
Lex.lean
|
feat: enable experimental module system in Init (#8047)
|
2025-04-23 17:21:33 +00:00 |
|
MapIdx.lean
|
feat: do not export private declarations (#8337)
|
2025-06-02 08:01:08 +00:00 |
|
Mem.lean
|
feat: enable experimental module system in Init (#8047)
|
2025-04-23 17:21:33 +00:00 |
|
Monadic.lean
|
fix: make Array.size not reducible (#8513)
|
2025-05-28 12:37:24 +00:00 |
|
OfFn.lean
|
fix: replace bad simp lemmas for Id (#7352)
|
2025-05-22 22:45:35 +00:00 |
|
Perm.lean
|
feat: do not export def bodies by default (#8221)
|
2025-05-15 12:16:54 +00:00 |
|
QSort.lean
|
chore: move Array.qsort to Basic file (#8177)
|
2025-04-30 13:32:05 +00:00 |
|
Range.lean
|
chore: initial @[grind] annotations for Array/Vector.range (#8606)
|
2025-06-03 06:44:01 +00:00 |
|
Set.lean
|
chore: remove >6 month old deprecations (#8514)
|
2025-05-28 11:28:03 +00:00 |
|
Subarray.lean
|
fix: replace bad simp lemmas for Id (#7352)
|
2025-05-22 22:45:35 +00:00 |
|
TakeDrop.lean
|
feat: do not export def bodies by default (#8221)
|
2025-05-15 12:16:54 +00:00 |
|
Zip.lean
|
chore: cleanup simp lemmas, following the simpNF linter (#8481)
|
2025-05-26 04:13:17 +00:00 |
