lean4-htt/src/Init/Data/Array
Joe Hendrix 9afca1c3a9
feat: port check_tactic commands from Std and add test cases (#3532)
This also adds several Array lemmas from std after cleaning up proofs
2024-02-28 23:32:54 +00:00
..
Basic.lean chore: upstream Std.Data.Array.Init.Basic (#3282) 2024-02-08 19:30:47 +00:00
BasicAux.lean refactor: termination_by changes in stdlib 2024-01-10 17:27:35 +01:00
BinSearch.lean chore: remove [Inhabited A] from binSearch / binInsert 2022-11-13 15:00:26 -08:00
DecidableEq.lean chore: upstream Std.Logic (#3312) 2024-02-14 09:40:55 +00:00
InsertionSort.lean feat: use sepBy1Indent for tactic blocks 2022-09-18 16:43:23 -07:00
Lemmas.lean feat: port check_tactic commands from Std and add test cases (#3532) 2024-02-28 23:32:54 +00:00
Mem.lean refactor: drop sizeOf_get_lt, duplicate of sizeOf_get (#3481) 2024-02-23 18:43:28 +00:00
QSort.lean refactor: termination_by changes in stdlib 2024-01-10 17:27:35 +01:00
Subarray.lean chore: upstream norm_cast tactic (#3322) 2024-02-19 17:49:17 -08:00