|
newfrontend
|
test: add tests/lean/newfrontend
|
2020-01-06 14:07:22 -08:00 |
|
run
|
feat: declare_syntax_cat without importing Init.Lean
|
2020-01-11 09:02:50 -08:00 |
|
mvar2.lean
|
chore: fix tests
|
2019-12-21 16:03:44 -08:00 |
|
mvar2.lean.expected.out
|
chore: fix tests
|
2019-12-21 16:03:44 -08:00 |
|
mvar3.lean
|
chore: fix tests
|
2019-12-21 16:03:44 -08:00 |
|
mvar3.lean.expected.out
|
chore: fix tests
|
2019-12-21 16:03:44 -08:00 |
|
StxQuot.lean
|
feat: command quotations
|
2020-01-06 10:09:26 -08:00 |
|
StxQuot.lean.expected.out
|
feat: command quotations
|
2020-01-06 10:09:26 -08:00 |