Scott Morrison
c656e71eb8
chore: make List.all and List.any short-circuit ( #2972 )
...
Changes the implementation of `List.all` and `List.any` so they
short-circuit. The implementations are tail-recursive.
This replaces https://github.com/leanprover/std4/pull/392 , which was
going to do this with `@[csimp]`.
2023-12-11 23:48:15 +00:00
Leni Aniva
ab36ed477e
feat: allow trailing comma in tuples, lists, and tactics ( #2643 )
2023-11-17 13:31:41 +01:00
Parth Shastri
642bc5d8f3
fix: replace DecidableEq with BEq/LawfulBEq in List mem theorems ( #2041 )
2023-10-30 14:03:16 +11:00
Bulhwi Cha
c1a58b212a
chore: remove whitespace ( #2244 )
...
Remove a duplicate whitespace character.
2023-05-31 06:00:42 -07:00
Jakob von Raumer
45b49e7f02
fix: typos
2023-05-05 12:07:54 -07:00
Sebastian Ullrich
042d14c470
fix: List.append_eq name
...
Fixes #2157
2023-03-19 10:28:48 +01:00
François G. Dorais
493a887cfb
fix: remove unnecessary hypothesis
2023-01-09 18:20:41 +01:00
Gabriel Dahia
b9f0062a58
doc: replace maximum? in minimum? docstring
...
This is my first contribution, if it can be counted as a contribution. Following the [documentation for simple fixes](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md#simple-fixes ), I opened the PR directly instead of discussing in the zulip or opening an issue. Hope that's ok.
2023-01-05 14:02:19 -08:00
Mario Carneiro
eb3b0377d7
fix: List.groupBy
2022-12-12 16:55:27 +01:00
Mario Carneiro
f74fee07e6
doc: document Init.Data.List.Basic ( #1828 )
...
* doc: document Init.Data.List.Basic
* Apply suggestions from code review
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2022-11-18 06:16:50 -08:00
Leonardo de Moura
b63eb886ce
chore: incorrect annotation
2022-11-07 16:18:36 -08:00
Leonardo de Moura
e55badef05
feat: List.mapMono
2022-10-24 19:50:09 -07:00
Gabriel Ebner
fc304d95c0
feat: Min/Max typeclasses
2022-10-21 14:36:38 -07:00
Gabriel Ebner
fb4d90a58b
feat: dynamic quotations for categories
2022-10-18 14:59:14 -07:00
Mario Carneiro
d4219c9d70
fix: List.Mem should have two parameters
2022-10-09 05:46:52 -07:00
Ed Ayers
2a6697e077
feat: goal-diffs ( #1610 )
2022-09-24 11:46:11 +02:00
Mario Carneiro
f6b3890dc5
feat: tail-recursive List.{mapM, foldrM}
2022-09-14 08:31:18 -07:00
Mario Carneiro
19a50a32ec
chore: remove List.init
2022-09-11 07:21:24 -07:00
Mario Carneiro
2886174dd0
chore: remove map₂, [specialize] zipWith
2022-09-11 07:21:24 -07:00
Mario Carneiro
ce3c0c0e6b
feat: add TR versions of Nat.{fold, any, all, repeat}
2022-08-31 17:52:59 -07:00
Leonardo de Moura
5df588cbbf
chore: remove unnecessary annotations
2022-08-02 05:42:53 -07:00
Mario Carneiro
25aea1b723
doc: document all the tactics
2022-08-01 08:08:03 -07:00
Sebastian Ullrich
f1f0f60768
fix: linter warnings
2022-07-29 10:31:19 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Henrik Böving
8932878274
feat: Functor instance for List
2022-07-21 08:08:48 -07:00
Gabriel Ebner
c100f45b77
feat: add simp lemmas and instances for LawfulBEq
2022-07-11 14:19:41 -07:00
Leonardo de Moura
2fcd406f99
chore: remove sorry
2022-07-10 20:04:06 -07:00
Leonardo de Moura
ee0735760a
feat: add instance : GetElem (List α) Nat α fun as i => i < as.length
2022-07-10 17:38:59 -07:00
Leonardo de Moura
220d2e3816
feat: add filterTR and [csimp] theorem
2022-06-24 06:40:38 -07:00
E.W.Ayers
a7c33a963f
doc: docstrings for List.isPrefixOf
2022-06-17 17:47:51 -07:00
François G. Dorais
bc206b2992
fix: LawfulBEq class
...
make arguments implicit and protect `LawfulBEq.rfl`
2022-06-16 15:33:32 -07:00
Leonardo de Moura
041827bed5
chore: unused variables
2022-06-07 17:54:10 -07:00
Sebastian Ullrich
fb2a2b3de2
fix: fixup previous commit
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Leonardo de Moura
34bbe5d12c
feat: add simp theorem List.of_toArray_eq_toArray (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
2022-05-27 18:26:48 -07:00
Leonardo de Moura
2a36ae4627
feat: add List.le_antisymm
2022-04-20 16:31:25 -07:00
Leonardo de Moura
9d55d7bf9e
feat: add helper tactic for applying List.sizeOf_lt_of_mem in termination proofs
2022-04-02 18:38:55 -07:00
Leonardo de Moura
03ec8cb30b
feat: missing sizeOf theorems for Array.get and List.get
2022-04-02 16:04:46 -07:00
Leonardo de Moura
cfb4e306f7
refactor: replace length_dropLast theorem
2022-04-01 16:44:24 -07:00
Leonardo de Moura
df3a8eb126
feat: add helper List.append simp theorems
2022-03-30 11:11:03 -07:00
casavaca
bf4ba1583d
feat: add simp theorem for List, (as.map f).length = as.length
2022-03-19 11:35:21 -07:00
Leonardo de Moura
cab3217b05
feat: add forIn'_eq_forIn theorem for lists
2022-03-14 11:50:47 -07:00
Leonardo de Moura
ef38c82c77
fix: missing hypotheses at List.sizeOf_lt_of_mem
2022-03-03 19:52:05 -08:00
Leonardo de Moura
99677823c3
fix: ForIn' instance binder annotations
2022-03-03 19:51:45 -08:00
Leonardo de Moura
d8ee03c1bb
feat: add ForIn' instance that is similar to ForIn but provides a proof that the iterated elements are in the collection
2022-03-03 19:05:27 -08:00
Leonardo de Moura
fd519401ff
feat: add Membership instance for List
...
and the theorem `a ∈ as -> sizeOf a < sizeOf as`.
We will use theorems like this one to improve the `decreasing_tactic`.
2022-03-03 18:13:21 -08:00
Leonardo de Moura
0f06fbf648
feat: LawfulBEq must be reflexive
2022-02-28 19:27:51 -08:00
Leonardo de Moura
b5f28239af
feat: add List helper theorems
2022-02-28 15:16:13 -08:00
Leonardo de Moura
b8bed6fb5c
feat: add LawfulBEq class
2022-02-25 13:35:08 -08:00
Leonardo de Moura
ba16903205
feat: add helper theorems
2022-02-19 21:25:44 -08:00
