Leonardo de Moura
|
9bb5d4dc93
|
chore: Nat.ltWf => Nat.lt_wf
|
2021-09-02 07:51:41 -07:00 |
|
Leonardo de Moura
|
2a6473641a
|
chore: fix theorem name
|
2021-08-30 10:10:54 -07:00 |
|
Leonardo de Moura
|
00193fb953
|
feat: add theorems for tutorial
|
2021-08-26 12:13:15 -07:00 |
|
Leonardo de Moura
|
795ccf6e2b
|
chore: add Trans instances for tutorial
|
2021-08-25 08:50:51 -07:00 |
|
Leonardo de Moura
|
f08b542068
|
chore: add Nat.add_mul and Nat.mul_add for tutorial
|
2021-08-25 06:44:12 -07:00 |
|
Leonardo de Moura
|
7066619123
|
refactor: define Nat.le using inductive type
|
2021-08-20 19:39:45 -07:00 |
|
Leonardo de Moura
|
a821dcbff2
|
chore: enforce naming convention for theorems
see issue #402
fix: `ElabTerm.lean`
|
2021-08-07 12:48:38 -07:00 |
|
Leonardo de Moura
|
f4a7ffd8c8
|
chore: fix codebase and tests
|
2021-06-29 17:14:52 -07:00 |
|
Sebastian Ullrich
|
a02c6fd3eb
|
chore: adapt stdlib & tests
|
2021-05-20 15:17:36 -07:00 |
|
Leonardo de Moura
|
c7096f54a2
|
feat: injectivity theorems for types defined in the prelude
|
2021-05-14 18:32:26 -07:00 |
|
Leonardo de Moura
|
8e81f03e3a
|
chore: adjust stdlib to recent changes
|
2021-05-06 15:43:56 -07:00 |
|
Sebastian Ullrich
|
aabb4a50aa
|
feat: remove bracket-less rw
|
2021-05-04 15:24:22 -07:00 |
|
Leonardo de Moura
|
ba5d622e59
|
chore: avoid case tactic
|
2021-05-01 19:50:50 -07:00 |
|
Leonardo de Moura
|
9f88ea8047
|
chore: remove old decide!, nativeRefl!, and nativeDecide!
|
2021-03-11 08:06:20 -08:00 |
|
Leonardo de Moura
|
9901898258
|
feat: add Nat.gcd
This commit also fix some theorem names to new naming convention.
|
2021-03-07 18:47:02 -08:00 |
|
Joe Hendrix
|
9bd60c7519
|
feat: Nat/Fin/UInt instances of bitwise classes
|
2021-03-04 15:42:43 -08:00 |
|
Leonardo de Moura
|
b9ef6f89a4
|
chore: cleanup
|
2021-02-26 19:34:39 -08:00 |
|
Leonardo de Moura
|
d1009e8405
|
chore: add simp lemmas, theorem naming convention
|
2021-02-16 11:53:49 -08:00 |
|
Leonardo de Moura
|
d734a2605b
|
chore: adjust stdlib
|
2020-11-29 17:01:56 -08:00 |
|
Leonardo de Moura
|
b72a3c69b6
|
fix: ambiguity at induction/cases
See efc3a320fe
|
2020-11-24 14:59:12 -08:00 |
|
Leonardo de Moura
|
304c80d610
|
feat: use <|
|
2020-11-19 09:03:38 -08:00 |
|
Leonardo de Moura
|
2537a2b84a
|
chore: implement list and array literals using syntax command
|
2020-11-11 13:50:25 -08:00 |
|
Leonardo de Moura
|
6ab0be952c
|
chore: merge src/Control files
Some of them were almost empty after the refactoring.
|
2020-11-10 18:47:23 -08:00 |
|
Leonardo de Moura
|
a8c791ecae
|
chore: remove dead files and functions
Remove obsolete combinators: `whenM`, `unlessM`, and `condM`
cc @Kha
|
2020-11-10 18:37:15 -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
|
c665d5e20a
|
chore: cleanup
|
2020-11-10 15:40:00 -08:00 |
|
Leonardo de Moura
|
2daeb195b5
|
chore: use new names
|
2020-11-10 10:15:19 -08:00 |
|
Leonardo de Moura
|
fa7fd4687c
|
feat: induction with multiple targets
|
2020-11-03 17:20:53 -08:00 |
|
Leonardo de Moura
|
bb99fc400a
|
chore: remove old crap
|
2020-11-02 19:16:23 -08:00 |
|
Leonardo de Moura
|
9932c79127
|
chore: cleanup
|
2020-11-02 17:27:34 -08:00 |
|
Leonardo de Moura
|
a0ab1b9eb4
|
chore: remove with
|
2020-11-02 13:35:26 -08:00 |
|
Leonardo de Moura
|
dfc346e76f
|
chore: remove obsolete attribute
|
2020-11-02 06:47:20 -08:00 |
|
Leonardo de Moura
|
6858cb5fb6
|
chore: cleanup
|
2020-10-29 10:24:16 -07: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
|
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
|
f7fcff56b8
|
chore: remove workaround
|
2020-10-24 16:48:43 -07:00 |
|
Leonardo de Moura
|
ffa1647bd5
|
chore: move to new frontend
|
2020-10-24 16:42:10 -07:00 |
|
Leonardo de Moura
|
522edc6743
|
chore: move to new frontend
|
2020-10-23 20:49:58 -07:00 |
|
Leonardo de Moura
|
afd53cab75
|
chore: move to new frontend
|
2020-10-23 17:36:29 -07:00 |
|
Leonardo de Moura
|
78c05e8f46
|
chore: move to new frontend
|
2020-10-23 16:13:55 -07:00 |
|
Leonardo de Moura
|
dd4ae81774
|
chore: move to new frontend
|
2020-10-16 09:16:33 -07:00 |
|
Sebastian Ullrich
|
386c706f3e
|
feat: basic parenthesizer
|
2020-05-04 14:28:36 -07:00 |
|
Leonardo de Moura
|
a8c3322ac8
|
doc: expand dependent pattern matching support for array literals
|
2020-03-13 06:39:13 -07:00 |
|
Leonardo de Moura
|
e9e4dfe1ff
|
feat: add new Coe.lean
|
2020-01-28 13:10:30 -08:00 |
|
Leonardo de Moura
|
7809274c3a
|
chore: Coe.lean ==> HasCoe.lean
|
2020-01-28 08:55:22 -08:00 |
|
Leonardo de Moura
|
67fb63c9fd
|
feat: use mpz_pow_ui to implement Nat.pow
|
2020-01-21 09:16:38 -08:00 |
|
Leonardo de Moura
|
2809cea147
|
chore: remove DecidableEq workaround
We have better indexing now.
|
2019-11-26 17:30:18 -08:00 |
|
Leonardo de Moura
|
c445199747
|
chore: library/Init ==> src/Init
cc @Kha @dselsam @cipher1024
|
2019-11-22 06:06:05 -08:00 |
|