max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/Data/Array
History
Kim Morrison ddd471223c
chore: cleaning up redundant simp lemmas (#5381) 
Problems reported by the simpNF linter downstream.
2024-09-18 10:06:29 +00:00
..
Subarray feat: show diffs when #guard_msgs fails (#3912) 2024-04-18 15:09:44 +00:00
Attach.lean chore: rename Array.data to Array.toList 2024-09-10 15:24:23 +10:00
Basic.lean chore: rename Array.data to Array.toList 2024-09-10 15:24:23 +10:00
BasicAux.lean chore: don't use simp_arith when simp will do (#5256) 2024-09-04 07:56:25 +00:00
BinSearch.lean chore: remove [Inhabited A] from binSearch / binInsert 2022-11-13 15:00:26 -08:00
Bootstrap.lean chore: rename Array.data to Array.toList 2024-09-10 15:24:23 +10:00
DecidableEq.lean fix: split (for if-expressions) should work on non-propositional goals (#4349) 2024-06-05 04:43:46 +00:00
InsertionSort.lean feat: use sepBy1Indent for tactic blocks 2022-09-18 16:43:23 -07:00
Lemmas.lean chore: cleaning up redundant simp lemmas (#5381) 2024-09-18 10:06:29 +00:00
Mem.lean chore: rename Array.data to Array.toList 2024-09-10 15:24:23 +10:00
QSort.lean perf: use with_reducible in special-purpose decreasing_trivial macros (#3991) 2024-04-29 15:12:27 +00:00
Subarray.lean feat: remove Decidable instances from GetElem (#4560) 2024-06-27 02:09:29 +00:00
TakeDrop.lean chore: rename Array.data to Array.toList 2024-09-10 15:24:23 +10:00