Kim Morrison 904404303b chore: robustify for byAsSorry (#6287) ... This PR makes some proofs more robust so they will still work with `byAsSorry`. Unfortunately, they are not a complete fix and there are remaining problems building with `byAsSorry`.		2024-12-02 23:53:16 +00:00
..
Subarray	feat: Array.swap takes Nat arguments, with tactic provided proofs (#6194)	2024-11-24 07:59:57 +00:00
Attach.lean	chore: robustify for byAsSorry (#6287)	2024-12-02 23:53:16 +00:00
Basic.lean	feat: Array.swap takes Nat arguments, with tactic provided proofs (#6194)	2024-11-24 07:59:57 +00:00
BasicAux.lean	feat: change Array.set to take a Nat and a tactic provided bound (#5988)	2024-11-11 07:53:24 +00:00
BinSearch.lean	feat: remove partial keyword and runtime bounds checks from Array.binSearch (#6193)	2024-11-24 06:08:16 +00:00
Bootstrap.lean	feat: add a coercion from List Nat to Lean.Meta.Occurrences (#6206)	2024-11-25 13:19:23 +00:00
DecidableEq.lean	feat: remove partial keyword and runtime bounds checks from Array.binSearch (#6193)	2024-11-24 06:08:16 +00:00
Find.lean	feat: duplicate List.attach/attachWith/pmap API for Array (#6132)	2024-11-20 01:16:48 +00:00
FinRange.lean	feat: upstream List.finRange from Batteries (#6234)	2024-11-27 04:27:22 +00:00
GetLit.lean	feat: relate Array.takeWhile with List.takeWhile (#5950)	2024-11-05 05:05:53 +00:00
InsertionSort.lean	feat: Array.swap takes Nat arguments, with tactic provided proofs (#6194)	2024-11-24 07:59:57 +00:00
Lemmas.lean	chore: missing Array/Vector injectivity lemmas (#6284)	2024-12-02 11:00:03 +00:00
MapIdx.lean	chore: review Array operations argument order (#6041)	2024-11-12 04:55:03 +00:00
Mem.lean	feat: change Array.get to take a Nat and a proof (#6032)	2024-11-12 03:30:46 +00:00
Monadic.lean	feat: lemmas about for loops over Array (#6055)	2024-11-13 23:23:55 +00:00
Perm.lean	feat: Array.swap_perm (#6272)	2024-12-01 08:35:28 +00:00
QSort.lean	feat: remove runtime bounds checks and partial from qsort (#6241)	2024-12-01 06:26:00 +00:00
Set.lean	feat: rename Array.setD to setIfInBounds (#6195)	2024-11-24 08:54:19 +00:00
Subarray.lean	chore: remove >6 month old deprecations (#6057)	2024-11-13 23:21:23 +00:00
TakeDrop.lean	feat: improve Array GetElem lemmas (#5465)	2024-09-25 07:17:13 +00:00