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
Leonardo de Moura
86328bcb9f
feat: tail recursive List.iota and [csimp] theorem
2022-02-16 11:25:46 -08:00
Mario Carneiro
f22f699d62
feat: split replicate / replicateTR with @[csimp]
2021-12-18 10:58:57 -08:00
Mario Carneiro
51a78fd7af
fix: change argument order of List.get[!?D]
2021-12-17 14:21:00 -08:00
Leonardo de Moura
f64753c106
test: simplify ac_expr.lean
...
We don't want to avoid proofs at `List.getIdx` and `Expr` when doing proofs by reflection.
The new encoding avoids that by using the fact that `vars` in
`Context` should never be empty.
To be honest, the best approach is still the old `unit`. We can just
rename it to `inhabitant` to make sure users don't assume it is the
unit of the AC operator. Then, we can just set it with the first element
of `vars` and avoid proofs at `denote`.
2021-10-06 17:56:26 -07:00
Leonardo de Moura
b205cfaaf2
chore: missing annotations at List.mapTR
2021-08-27 10:17:49 -07:00
Leonardo de Moura
8ba10521e6
feat: add theorem for tutorial
2021-08-26 12:58:02 -07:00
Leonardo de Moura
00193fb953
feat: add theorems for tutorial
2021-08-26 12:13:15 -07:00
Leonardo de Moura
4dccaa963b
feat: add List.mapTR and csimp lemma
2021-08-22 09:32:19 -07:00
Leonardo de Moura
ec6af1ba26
feat: use simple List.append definition and add csimp theorem
2021-08-21 16:11:54 -07:00
Leonardo de Moura
3b240d9a14
feat: use simple List.length definition and add csimp theorem
2021-08-21 13:11:06 -07:00
Leonardo de Moura
af5ff9ceb2
refactor: move List.takeWhile to Init.Data.List.Basic
...
Motivation: make sure it will be aligned by BinPort
2021-07-31 15:03:33 -07:00
Leonardo de Moura
f4a7ffd8c8
chore: fix codebase and tests
2021-06-29 17:14:52 -07:00
Sebastian Ullrich
693c2ccf71
feat: min, max, List.min/maximum?
2021-05-30 17:29:54 +02:00
Leonardo de Moura
3a80e87793
chore: #405 step 1
2021-04-22 20:03:48 -07:00
Leonardo de Moura
091fadbf64
feat: add List.rotateLeft and List.rotateRight
2021-03-12 17:09:22 -08:00
Leonardo de Moura
4aec7579db
test: add do equivalence examples
2021-03-03 13:44:30 -08:00
Leonardo de Moura
228bc2dd54
refactor: Traversable => ForM
2021-03-02 06:22:22 -08:00
Leonardo de Moura
35e1f5ad97
refactor: Foldable => Traversable
2021-02-28 16:11:20 -08:00
Leonardo de Moura
9d9f14cd5e
chore: mark List.foldlM as protected
2021-02-28 09:14:37 -08:00
Leonardo de Moura
ef4d5950ae
feat: add Foldable typeclass
...
We use it in the "`do` unchained" paper.
It will eventually replace `ForIn`.
2021-02-28 09:00:52 -08:00
Leonardo de Moura
d1009e8405
chore: add simp lemmas, theorem naming convention
2021-02-16 11:53:49 -08:00
Leonardo de Moura
aae8a35150
feat: add ForIn type class
2021-02-04 17:59:44 -08:00
Sebastian Ullrich
0c91b3769e
chore: replace variables in src/
2021-01-22 14:36:05 +01:00
Leonardo de Moura
539c43e153
fix: typo
...
closes #238
2020-12-28 15:55:25 -08:00
Leonardo de Moura
d734a2605b
chore: adjust stdlib
2020-11-29 17:01:56 -08:00
Leonardo de Moura
0869f38de4
chore: update structure, class, inductive
2020-11-27 15:09:30 -08:00
Leonardo de Moura
6f0919f08d
chore: fix places that require erewrite
2020-11-25 11:02:26 -08:00
Leonardo de Moura
9023e93b3e
refactor: move Array.set to Prelude
2020-11-25 11:02:25 -08:00
Leonardo de Moura
b72a3c69b6
fix: ambiguity at induction/cases
...
See efc3a320fe
2020-11-24 14:59:12 -08:00
