lean4-htt/src/Init/Data/List
Kim Morrison f1b2850aa4
chore: split Init.Data.Array.Lemmas for better bootstrapping (#5255)
This allows significantly reducing the imports of `Init.Data.List.Impl`.
2024-09-04 08:33:13 +00:00
..
Nat chore: remove redundant simp annotations (#5251) 2024-09-04 04:36:09 +00:00
Sort chore: cleanup imports of Array.Lemmas (#5246) 2024-09-04 01:48:14 +00:00
Attach.lean chore: remove @[simp] from List.getLast_eq_iff_getLast_eq_some (#5178) 2024-08-27 03:23:39 +00:00
Basic.lean chore: move @[csimp] lemmas earlier where possible (#5214) 2024-08-30 06:42:05 +00:00
BasicAux.lean chore: don't use simp_arith when simp will do (#5256) 2024-09-04 07:56:25 +00:00
Control.lean feat: upstream more List lemmas (#4856) 2024-07-28 23:23:59 +00:00
Count.lean chore: cleanup #5167 workarounds after update stage0 (#5175) 2024-08-26 17:53:30 +00:00
Erase.lean feat: List.Pairwise_erase and related lemmas (#5196) 2024-08-28 23:11:02 +00:00
Find.lean chore: remove @[simp] from List.getLast_eq_iff_getLast_eq_some (#5178) 2024-08-27 03:23:39 +00:00
Impl.lean chore: split Init.Data.Array.Lemmas for better bootstrapping (#5255) 2024-09-04 08:33:13 +00:00
Lemmas.lean chore: split Init.Data.Array.Lemmas for better bootstrapping (#5255) 2024-09-04 08:33:13 +00:00
MinMax.lean chore: split Init.Data.List.Lemmas (#4863) 2024-07-30 03:17:34 +00:00
Monadic.lean chore: split Init.Data.List.Lemmas (#4863) 2024-07-30 03:17:34 +00:00
Nat.lean feat: new+old lemmas about List.Sublist (#5029) 2024-08-14 04:13:57 +00:00
Notation.lean chore: reorganisation of List API (#4469) 2024-06-17 04:21:53 +00:00
Pairwise.lean chore: cleanup #5167 workarounds after update stage0 (#5175) 2024-08-26 17:53:30 +00:00
Perm.lean chore: running the simpNF linter over Lean (#5133) 2024-08-24 07:10:07 +00:00
Range.lean chore: cleanup imports of Array.Lemmas (#5246) 2024-09-04 01:48:14 +00:00
Sort.lean feat: List.mergeSort (#5092) 2024-08-20 06:32:52 +00:00
Sublist.lean feat: allow users to disable simpCtorEq simproc (#5167) 2024-08-26 13:51:21 +00:00
TakeDrop.lean chore: running the simpNF linter over Lean (#5133) 2024-08-24 07:10:07 +00:00
Zip.lean feat: misc List lemma updates (#5127) 2024-08-23 01:17:17 +00:00