Gabriel Ebner
|
7356840cbc
|
feat: use sepBy1Indent for tactic blocks
|
2022-09-18 16:43:23 -07:00 |
|
Leonardo de Moura
|
e4b358a01e
|
refactor: prepare to elaborate a[i] notation using typeclasses
|
2022-07-09 15:24:22 -07:00 |
|
Leonardo de Moura
|
5e3a3a6c21
|
chore: remove notation a[i,h] for a[⟨i, h⟩]
|
2022-07-03 06:24:26 -07:00 |
|
Leonardo de Moura
|
a2456c3a0f
|
feat: add notation a[i, h] for a[⟨i, h⟩]
|
2022-07-02 15:50:49 -07:00 |
|
Leonardo de Moura
|
bd89bdde8a
|
fix: core library
see #1018
|
2022-02-15 12:12:56 -08: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 |
|
Sebastian Ullrich
|
a02c6fd3eb
|
chore: adapt stdlib & tests
|
2021-05-20 15:17:36 -07:00 |
|
Sebastian Ullrich
|
aabb4a50aa
|
feat: remove bracket-less rw
|
2021-05-04 15:24:22 -07:00 |
|
Leonardo de Moura
|
d1009e8405
|
chore: add simp lemmas, theorem naming convention
|
2021-02-16 11:53:49 -08:00 |
|
Leonardo de Moura
|
7c865e7bd9
|
feat: sort instances by priority
|
2020-12-16 10:45:27 -08:00 |
|
Leonardo de Moura
|
fe08b28c7c
|
feat: add Array.insertionSort
|
2020-12-16 10:45:27 -08:00 |
|