Mario Carneiro
|
ce3c0c0e6b
|
feat: add TR versions of Nat.{fold, any, all, repeat}
|
2022-08-31 17:52:59 -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
|
cfb4e306f7
|
refactor: replace length_dropLast theorem
|
2022-04-01 16:44:24 -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
|
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
|
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 |
|
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
|
d1009e8405
|
chore: add simp lemmas, theorem naming convention
|
2021-02-16 11:53:49 -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 |
|
Leonardo de Moura
|
c7a31ed52e
|
chore: remove duplicate instances
|
2020-11-21 11:05:52 -08:00 |
|
Leonardo de Moura
|
c305c2691f
|
chore: use :=
|
2020-11-19 07:22:31 -08:00 |
|
Leonardo de Moura
|
7e533b4650
|
refactor: use Lists for Array reference implementation
Motivation: better reduction in the kernel.
cc @Kha
|
2020-11-17 17:05:53 -08:00 |
|
Leonardo de Moura
|
cca3bad0bb
|
feat: add Prelude.lean
`Prelude.lean` has no dependencies, and
at the end of `Prelude`, the `syntax` and `macro` commands are operational.
|
2020-11-10 18:08:18 -08:00 |
|
Leonardo de Moura
|
2daeb195b5
|
chore: use new names
|
2020-11-10 10:15:19 -08:00 |
|
Leonardo de Moura
|
898a08a0c1
|
chore: avoid Has prefix in type classes
closes #203
|
2020-10-27 18:29:19 -07:00 |
|
Leonardo de Moura
|
97c93ec557
|
chore: prepare to rename
|
2020-10-27 18:09:03 -07:00 |
|
Leonardo de Moura
|
13c2a8ff51
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Leonardo de Moura
|
1d338c4fc4
|
chore: move Core.lean to new frontend
|
2020-10-25 08:54:37 -07:00 |
|
Leonardo de Moura
|
35f0bf7d77
|
chore: move to new frontend
|
2020-10-24 16:21:23 -07:00 |
|
Sebastian Ullrich
|
ed14375dad
|
feat: sort and deduplicate "expected" tokens in parser error messages
|
2020-03-19 17:17:08 -07:00 |
|
Sebastian Ullrich
|
e999fa678d
|
feat: add some useful helper functions I didn't actually use in the end
|
2020-03-19 17:14:31 -07:00 |
|