Joachim Breitner 6d22793ddf refactor: Array.feraseIdx: avoid have in definition (#4074) ... otherwise it remains in the equational theorem and may cause the “unused have linter” to trigger. By moving the proof into `decreasing_by`, the equational theorems are unencumbered by termination arguments. see also https://github.com/leanprover/std4/pull/690#issuecomment-2095378609		2024-05-06 08:08:43 +00:00
..
Subarray	feat: show diffs when #guard_msgs fails (#3912)	2024-04-18 15:09:44 +00:00
Basic.lean	refactor: Array.feraseIdx: avoid have in definition (#4074)	2024-05-06 08:08:43 +00:00
BasicAux.lean	perf: use with_reducible in special-purpose decreasing_trivial macros (#3991)	2024-04-29 15:12:27 +00:00
BinSearch.lean	chore: remove [Inhabited A] from binSearch / binInsert	2022-11-13 15:00:26 -08:00
DecidableEq.lean	perf: use with_reducible in special-purpose decreasing_trivial macros (#3991)	2024-04-29 15:12:27 +00:00
InsertionSort.lean	feat: use sepBy1Indent for tactic blocks	2022-09-18 16:43:23 -07:00
Lemmas.lean	feat: upstream lemmas about basic List/Array operations (#4059)	2024-05-06 03:52:33 +00:00
Mem.lean	perf: use with_reducible in special-purpose decreasing_trivial macros (#3991)	2024-04-29 15:12:27 +00: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: show diffs when #guard_msgs fails (#3912)	2024-04-18 15:09:44 +00:00