Leonardo de Moura
|
ac440aa6ea
|
chore: update stage0
|
2020-12-14 17:34:18 -08:00 |
|
Leonardo de Moura
|
69e8385f8d
|
refactor: move prioParser to Term.lean
|
2020-12-14 17:33:38 -08:00 |
|
Leonardo de Moura
|
c0b90e9341
|
chore: update stage0
|
2020-12-14 17:29:04 -08:00 |
|
Leonardo de Moura
|
0004196977
|
feat: add attrParam builtin parsers
|
2020-12-14 17:27:28 -08:00 |
|
Leonardo de Moura
|
4811a207e6
|
chore: update stage0
|
2020-12-14 16:46:44 -08:00 |
|
Leonardo de Moura
|
a3fe907a28
|
feat: add attrParam syntax category
cc @Kha
|
2020-12-14 16:45:05 -08:00 |
|
Leonardo de Moura
|
f5de22ee36
|
chore: fix tests
|
2020-12-14 16:34:06 -08:00 |
|
Leonardo de Moura
|
c0470e407e
|
chore: update stage0
|
2020-12-14 16:29:45 -08:00 |
|
Leonardo de Moura
|
abe7481453
|
feat: elaborate prio DSL
|
2020-12-14 16:25:10 -08:00 |
|
Leonardo de Moura
|
a2afd10060
|
feat: prio DSL
|
2020-12-14 16:07:02 -08:00 |
|
Leonardo de Moura
|
7e6a9fa53a
|
chore: update stage0
|
2020-12-14 16:04:50 -08:00 |
|
Leonardo de Moura
|
acba8d4a4a
|
chore: cleanup
|
2020-12-14 16:01:52 -08:00 |
|
Leonardo de Moura
|
6909faf4a2
|
chore: update stage0
|
2020-12-14 15:37:02 -08:00 |
|
Leonardo de Moura
|
fcaf38d566
|
fix: handle prec DSL at infixl macro
|
2020-12-14 15:35:37 -08:00 |
|
Leonardo de Moura
|
68f943a753
|
chore: update stage0
|
2020-12-14 15:16:44 -08:00 |
|
Leonardo de Moura
|
a46505cb8b
|
feat: use new precedence syntax
|
2020-12-14 15:14:03 -08:00 |
|
Leonardo de Moura
|
911a433010
|
chore: remove temp comments
|
2020-12-14 15:10:41 -08:00 |
|
Leonardo de Moura
|
eddacf6b09
|
chore: update stage0
|
2020-12-14 15:06:28 -08:00 |
|
Leonardo de Moura
|
f95a450894
|
feat: add builtin prec/prio parsers
|
2020-12-14 15:05:39 -08:00 |
|
Leonardo de Moura
|
cfb60c0cf3
|
chore: avoid auto generated names
|
2020-12-14 14:49:34 -08:00 |
|
Leonardo de Moura
|
fd2bd91709
|
chore: update stage0
|
2020-12-14 13:45:05 -08:00 |
|
Leonardo de Moura
|
65bb478f7a
|
feat: expand prec.quot and prio.quot, add helper command macro elabStxQuot!
|
2020-12-14 13:36:26 -08:00 |
|
Leonardo de Moura
|
046f4866b6
|
chore: update stage0
|
2020-12-14 13:26:30 -08:00 |
|
Leonardo de Moura
|
7d1d7dc171
|
feat: prec DSL
|
2020-12-14 13:25:08 -08:00 |
|
Leonardo de Moura
|
216d34e178
|
feat: add prio parser category
|
2020-12-14 13:24:56 -08:00 |
|
Leonardo de Moura
|
35f9518559
|
chore: update stage0
|
2020-12-14 13:09:27 -08:00 |
|
Leonardo de Moura
|
c5e201bce6
|
feat: add prec syntax category
|
2020-12-14 13:09:27 -08:00 |
|
Leonardo de Moura
|
469c9b7bbf
|
chore: remove TODO
|
2020-12-14 11:50:22 -08:00 |
|
Leonardo de Moura
|
9936040087
|
chore: fix test
TODO: add instance priorities.
|
2020-12-14 10:47:44 -08:00 |
|
Leonardo de Moura
|
5a5a49a54a
|
feat: add class abbrev macro
|
2020-12-14 10:19:00 -08:00 |
|
Leonardo de Moura
|
f24fff7985
|
chore: remove temporary workaround
|
2020-12-14 10:08:29 -08:00 |
|
Leonardo de Moura
|
0b58ebfba2
|
chore: update stage0
|
2020-12-14 10:07:37 -08:00 |
|
Leonardo de Moura
|
a0463e8fa8
|
feat: elaborate new stactic quotations
|
2020-12-14 09:28:04 -08:00 |
|
Leonardo de Moura
|
186e4fa788
|
chore: update stage0
|
2020-12-14 09:23:43 -08:00 |
|
Leonardo de Moura
|
ac692bfc79
|
feat: add new static quotations
For users that are writing (not-trivial) macros without `import Lean`.
cc @Kha
|
2020-12-14 09:21:26 -08:00 |
|
Leonardo de Moura
|
c7a8fa2629
|
chore: expose a few auxiliary command parsers
|
2020-12-14 09:15:26 -08:00 |
|
Leonardo de Moura
|
4001407f10
|
refactor: add MonadError class abbreviation
|
2020-12-14 09:15:26 -08:00 |
|
Sebastian Ullrich
|
9a6af0f39f
|
test: simplify beginEndAsMacro
|
2020-12-14 17:45:30 +01:00 |
|
Sebastian Ullrich
|
314c5c9d41
|
feat: run single non-category quotation under interpreter as well
|
2020-12-14 17:13:59 +01:00 |
|
Sebastian Ullrich
|
a9bdb2f70a
|
feat: prefer interpreter for running builtin parsers in quotations
|
2020-12-14 16:45:32 +01:00 |
|
Sebastian Ullrich
|
a914176897
|
test: fix...
|
2020-12-14 15:41:24 +01:00 |
|
Sebastian Ullrich
|
f641a660ce
|
doc: include up-to-date begin-end macro code from test
@leodemoura: #include is pretty handy
|
2020-12-14 15:10:03 +01:00 |
|
Sebastian Ullrich
|
3543cae8e8
|
chore: CI: verbose output for Build manual
|
2020-12-14 14:53:36 +01:00 |
|
Sebastian Ullrich
|
7dc08328bb
|
chore: update stage0
|
2020-12-14 13:55:01 +01:00 |
|
Sebastian Ullrich
|
0316c872b9
|
feat: macro: use appropriate antiquotation kind dependent on bound syntax
/cc @leodemoura
|
2020-12-14 13:54:34 +01:00 |
|
Leonardo de Moura
|
35eac0f232
|
chore: update stage0
|
2020-12-13 16:30:39 -08:00 |
|
Leonardo de Moura
|
0d9694d836
|
chore: user deriving BEq
|
2020-12-13 16:30:07 -08:00 |
|
Leonardo de Moura
|
3c06d69190
|
chore: update stage0
|
2020-12-13 16:15:26 -08:00 |
|
Leonardo de Moura
|
bad714f5e9
|
feat: add deriving BEq
|
2020-12-13 16:13:27 -08:00 |
|
Leonardo de Moura
|
0862df9ade
|
fix: missing ppSpace at set_option parser
|
2020-12-13 15:52:03 -08:00 |
|