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 |
|
Leonardo de Moura
|
15232f51d3
|
feat: add Expr.constainsFVar
|
2020-12-13 15:51:48 -08:00 |
|
Leonardo de Moura
|
731ca49088
|
chore: cleanup
|
2020-12-13 15:51:34 -08:00 |
|
Leonardo de Moura
|
f5d59ee287
|
fix: missing eraseMacroScopes at set_option
|
2020-12-13 15:51:00 -08:00 |
|
Leonardo de Moura
|
ed86e74149
|
feat: add option match.ignoreUnusedAlts
It is useful for macros that generate `match`-expressions
|
2020-12-13 15:50:24 -08:00 |
|
Leonardo de Moura
|
d6ba0592d1
|
chore: remove dead code
|
2020-12-13 15:50:08 -08:00 |
|
Leonardo de Moura
|
f345c8c708
|
feat: add betaReduce
|
2020-12-13 15:49:22 -08:00 |
|
Leonardo de Moura
|
04a07c15b9
|
chore: use deriving Inhabited
|
2020-12-13 11:57:59 -08:00 |
|
Leonardo de Moura
|
b05a633029
|
chore: update stage0
|
2020-12-13 11:11:57 -08:00 |
|
Leonardo de Moura
|
bbafaf8805
|
fix: Array.mk and Array.data externs
|
2020-12-13 11:10:01 -08:00 |
|
Leonardo de Moura
|
3b6d65c3c3
|
chore: use deriving Inhabited
|
2020-12-13 10:09:20 -08:00 |
|
Leonardo de Moura
|
f885b30515
|
chore: update stage0
|
2020-12-13 09:06:37 -08:00 |
|
Leonardo de Moura
|
0bbc2ca884
|
feat: elaborate optDeriving
|
2020-12-13 09:05:03 -08:00 |
|
Leonardo de Moura
|
2a653743a1
|
test: simple test for deriving Inhabited
TODO: elaborate `optDeriving` suffix to `inductive/structure` commands
|
2020-12-12 18:58:56 -08:00 |
|
Leonardo de Moura
|
8fd6870931
|
fix: optDeriving parser
|
2020-12-12 18:58:44 -08:00 |
|
Leonardo de Moura
|
ebd8680de8
|
feat: add Deriving/Inhabited.lean
|
2020-12-12 18:52:24 -08:00 |
|
Leonardo de Moura
|
2c81d7e91c
|
feat: add basic deriving instance elaborator
|
2020-12-12 17:00:49 -08:00 |
|
Leonardo de Moura
|
1bc773587f
|
chore: update stage0
|
2020-12-12 16:49:49 -08:00 |
|
Leonardo de Moura
|
01ec581617
|
chore: update deriving instance syntax
|
2020-12-12 16:48:12 -08:00 |
|
Leonardo de Moura
|
fb175ccab7
|
feat: add Deriving.lean
|
2020-12-12 16:08:50 -08:00 |
|
Leonardo de Moura
|
f4a51ac201
|
chore: add deriving to keyword lists
|
2020-12-12 15:42:01 -08:00 |
|
Leonardo de Moura
|
3e95f1fcb0
|
chore: update stage0
|
2020-12-12 15:39:19 -08:00 |
|
Leonardo de Moura
|
3743f877f4
|
feat: add deriving parsers
|
2020-12-12 15:33:36 -08:00 |
|
Leonardo de Moura
|
e9a1c3ac44
|
test: deriving experiment
|
2020-12-12 15:26:55 -08:00 |
|
Leonardo de Moura
|
5249fdc24d
|
chore: cleanup and style
|
2020-12-12 10:36:26 -08:00 |
|
Leonardo de Moura
|
9333fb4cf6
|
chore: style
|
2020-12-12 08:34:00 -08:00 |
|
Leonardo de Moura
|
bb8cd95437
|
chore: update-stage0
|
2020-12-12 08:28:40 -08:00 |
|
Sebastian Ullrich
|
554d0b4d4c
|
chore: adapt stdlib to new antiquotation splices
|
2020-12-12 17:20:03 +01:00 |
|
Sebastian Ullrich
|
331b987f8b
|
chore: update stage0
|
2020-12-12 16:02:59 +01:00 |
|
Sebastian Ullrich
|
8dfa588983
|
feat: introduce SepArray and use it for sepBy antiquotation splices
|
2020-12-12 16:02:15 +01:00 |
|
Sebastian Ullrich
|
9e06680541
|
chore: remove old antiquotations splice syntax
|
2020-12-12 14:57:14 +01:00 |
|
Sebastian Ullrich
|
a13f129312
|
feat: antiquotation suffix splices such as $x:k,*
/cc @leodemoura
|
2020-12-12 14:57:14 +01:00 |
|