lean4-htt/src/Init/Data/List
2024-08-26 03:04:58 +00:00
..
Nat feat: head/getLast lemmas for List.range (#5158) 2024-08-26 01:48:45 +00:00
Sort feat: Nat.add_left_eq_self and relatives (#5104) 2024-08-21 04:11:57 +00:00
Attach.lean feat: more lemmas about List.pmap/attach (#5160) 2024-08-26 02:15:58 +00:00
Basic.lean chore: running the simpNF linter over Lean (#5133) 2024-08-24 07:10:07 +00:00
BasicAux.lean chore: running the simpNF linter over Lean (#5133) 2024-08-24 07:10:07 +00:00
Control.lean feat: upstream more List lemmas (#4856) 2024-07-28 23:23:59 +00:00
Count.lean feat: more List.Sublist theorems (#5048) 2024-08-15 05:38:25 +00:00
Erase.lean feat: lemmas about List.erase(|P|Idx) (#5152) 2024-08-25 07:01:46 +00:00
Find.lean feat: more lemmas about List.pmap/attach (#5160) 2024-08-26 02:15:58 +00:00
Impl.lean feat: upstream more List operations (#4855) 2024-07-28 04:52:21 +00:00
Lemmas.lean feat: more improvements to List simp confluence (#5163) 2024-08-26 03:04:58 +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 feat: List.mergeSort (#5092) 2024-08-20 06:32:52 +00:00
Perm.lean chore: running the simpNF linter over Lean (#5133) 2024-08-24 07:10:07 +00:00
Range.lean feat: more List.find?/findSome?/findIdx? theorems (#5053) 2024-08-15 11:53:35 +00:00
Sort.lean feat: List.mergeSort (#5092) 2024-08-20 06:32:52 +00:00
Sublist.lean feat: improving confluence of List simp lemmas (#5151) 2024-08-25 04:32:45 +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