Leonardo de Moura
|
0e8c8784a5
|
feat: elaborate notation
|
2020-01-15 20:53:24 -08:00 |
|
Leonardo de Moura
|
f919041400
|
feat: expand precedence
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
6ff732f698
|
refactor: move notation comands to Syntax.lean
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
d9c6624a0a
|
feat: add support for trailing syntax
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
b9c161b30c
|
feat: elaborate macro command
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
b14c7cb69b
|
feat: allow user to set nodeKind at syntax command
|
2020-01-14 18:51:31 -08:00 |
|
Leonardo de Moura
|
664172d266
|
feat: elaborate syntax command
|
2020-01-14 18:18:43 -08:00 |
|
Leonardo de Moura
|
2d83d49341
|
refactor: add Elab/Syntax.lean
|
2020-01-14 14:22:55 -08:00 |
|