| .. |
|
Lex
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Subarray
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Attach.lean
|
feat: align List/Array/Vector.any/all theorems (#7249)
|
2025-02-26 23:53:53 +00:00 |
|
Basic.lean
|
chore: cleanup of remaining Array-specific material (#7253)
|
2025-02-27 10:51:30 +00:00 |
|
BasicAux.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
BinSearch.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Bootstrap.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Count.lean
|
chore: cleanup of remaining Array-specific material (#7253)
|
2025-02-27 10:51:30 +00:00 |
|
DecidableEq.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Erase.lean
|
chore: cleanup of remaining Array-specific material (#7253)
|
2025-02-27 10:51:30 +00:00 |
|
Extract.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Find.lean
|
feat: add Array/Vector.replace (#7235)
|
2025-02-26 06:03:45 +00:00 |
|
FinRange.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
GetLit.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
InsertIdx.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
InsertionSort.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Lemmas.lean
|
feat: lemmas about pure for {List,Array,Vector}.{mapM,foldlM,foldrM,anyM,allM,findM?,findSomeM?} (#7356)
|
2025-03-10 13:55:17 +00:00 |
|
Lex.lean
|
feat: lemmas about lexicographic order on Array and Vector (#6399)
|
2024-12-19 10:36:50 +00:00 |
|
MapIdx.lean
|
chore: cleanup of remaining Array-specific material (#7253)
|
2025-02-27 10:51:30 +00:00 |
|
Mem.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Monadic.lean
|
feat: lemmas about pure for {List,Array,Vector}.{mapM,foldlM,foldrM,anyM,allM,findM?,findSomeM?} (#7356)
|
2025-03-10 13:55:17 +00:00 |
|
OfFn.lean
|
chore: cleanup of remaining Array-specific material (#7253)
|
2025-02-27 10:51:30 +00:00 |
|
Perm.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
QSort.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Range.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Set.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Subarray.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
TakeDrop.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
|
Zip.lean
|
chore: re-enable List variable linter (#7215)
|
2025-02-24 23:34:01 +00:00 |
9a435b4f4a