Sebastian Ullrich
|
11f04c9397
|
feat: syntax quotation parsers
|
2019-12-10 22:02:39 +01:00 |
|
Leonardo de Moura
|
9716208a90
|
feat: elaborate list notation
|
2019-12-09 17:09:23 -08:00 |
|
Leonardo de Moura
|
fd141d152b
|
fix: ensure binderType has an uniform representation
|
2019-12-09 16:47:24 -08:00 |
|
Leonardo de Moura
|
92958e8d66
|
refactor: remove Syntax.other
We are going to use synthetic metavariables for postponing elaboration.
|
2019-12-06 09:23:44 -08:00 |
|
Leonardo de Moura
|
68e18937b2
|
chore: remove #preterm
|
2019-12-05 11:38:53 -08:00 |
|
Leonardo de Moura
|
cc5a3cca29
|
chore: move helper modules to src/Init/Lean/Util
|
2019-12-04 17:17:34 -08:00 |
|
Leonardo de Moura
|
f15af1df0a
|
chore: move Lean auxiliary datatypes to src/Init/Lean/Data
|
2019-12-04 17:00:13 -08:00 |
|
Leonardo de Moura
|
dacf69b2f0
|
chore: remove mkCApp* functions
|
2019-12-04 13:07:42 -08:00 |
|
Leonardo de Moura
|
c445199747
|
chore: library/Init ==> src/Init
cc @Kha @dselsam @cipher1024
|
2019-11-22 06:06:05 -08:00 |
|