Leonardo de Moura
f20d4aaa83
fix: avoid termParser at mkAntiquot
...
@kha `mkAntiquot` is used in all categories. I removed
`termParser (appPrec + 1)` to avoid nasty interactions between
`termParser` and the surrounding category.
This commity ensures the antiquotation prefix is one of the following
forms `$<id>` or `$(<term>)`.
I made the two cases look like term syntax because I didn't want to
change your expander. We should fix this next week.
2020-01-20 10:19:16 -08:00
Leonardo de Moura
9425ec6a06
chore: remove workaround
2020-01-20 09:58:13 -08:00
Leonardo de Moura
1665cea8e9
fix: antiquotation ambiguity
2020-01-20 09:53:49 -08:00
Leonardo de Moura
b5fc9c19fe
feat add evalIntros
2020-01-19 17:48:19 -08:00
Simon Hudon
c0a7495495
feat: MonadIO now extends MonadExcept IO.Error
2020-01-19 17:23:37 -08:00
Simon Hudon
961861ceab
fix: thread local storage of std streams
2020-01-19 17:23:24 -08:00
Simon Hudon
bd87ea5d5e
feat: override standard streams
2020-01-19 17:23:12 -08:00
Simon Hudon
7575a32035
feat: add std streams
...
This reverts commit 021ce21d5f70c2efcc58a0588ed6dc4999be6a33.
2020-01-19 17:22:58 -08:00
Leonardo de Moura
81c26214c5
feat: expand repeat
2020-01-19 17:06:19 -08:00
Leonardo de Moura
e931fac3bb
feat: add evalTry
2020-01-19 16:52:39 -08:00
Leonardo de Moura
b94e0381ad
feat: add evalSkip and evalTraceState
2020-01-19 16:37:01 -08:00
Leonardo de Moura
038ffcffc3
fix: TacticM should not see pending syntheticMVars from caller
2020-01-19 16:27:40 -08:00
Leonardo de Moura
0a3e9abccb
feat: eval apply tactic
2020-01-19 16:23:32 -08:00
Leonardo de Moura
03fb591604
feat: add findMVar?
2020-01-19 16:03:01 -08:00
Leonardo de Moura
b577ff2073
feat: add renameMVar and improve forallMetaTelescopeReducingAux
2020-01-19 15:48:42 -08:00
Leonardo de Moura
0d25c5f55c
feat: add Array.filterM
2020-01-19 15:18:01 -08:00
Leonardo de Moura
4638b6589e
chore: add mayPostpone
2020-01-19 14:44:47 -08:00
Leonardo de Moura
e57d3431ee
refactor: move basic Syntax API to LeanInit
...
We want to make them available for `macro`-building
2020-01-19 14:44:03 -08:00
Leonardo de Moura
b2c92d57b3
feat: add withReducible
2020-01-19 14:24:11 -08:00
Leonardo de Moura
312ea061b1
chore: use toExpr
...
cc @Kha
2020-01-19 11:58:17 -08:00
Sebastian Ullrich
6e1d70aaf2
feat: elaborate quoted names
2020-01-19 11:58:17 -08:00
Sebastian Ullrich
6c2a2cfa35
feat: support postfix syntax in macro
2020-01-19 11:58:17 -08:00
Sebastian Ullrich
3ee99b5859
feat: remove last superscript letter from list of valid identifier chars
2020-01-19 11:58:17 -08:00
Leonardo de Moura
655da9baef
fix: tag refine subgoals
2020-01-19 11:58:17 -08:00
Sebastian Ullrich
15bed7c95c
chore: support old notation syntax
2020-01-19 18:45:08 +01:00
Sebastian Ullrich
7f4e1db86b
refactor: replace mkTermIdFromIdent with antiquotation kind where possible
2020-01-19 08:28:49 -08:00
Sebastian Ullrich
9790b2b390
fix: hygienic mkTermId for constants
2020-01-19 08:28:49 -08:00
Leonardo de Moura
cec66bc75c
feat: add a few helper tactics
2020-01-19 08:28:43 -08:00
Leonardo de Moura
86edc94dbe
feat: add support for elaborating raw literals
2020-01-18 20:02:50 -08:00
Leonardo de Moura
3b8e1f8591
feat: add char (literal) as valid macro argument type
2020-01-18 19:43:19 -08:00
Leonardo de Moura
58b21fe0c9
feat: mark literals as valid kinds
2020-01-18 19:41:40 -08:00
Leonardo de Moura
be571e8d42
feat: elaborate new macro argument types
2020-01-18 19:41:17 -08:00
Leonardo de Moura
ac2fb7e149
feat: allow ident, num (numeric literals) and str (string literals) as macro argument types
2020-01-18 19:19:18 -08:00
Leonardo de Moura
60a9aa52c5
feat: add Array.getSepElems
...
cc @Kha
2020-01-18 19:12:44 -08:00
Leonardo de Moura
3e86608ce2
fix: erase macro scopes from parser categories
2020-01-18 19:10:35 -08:00
Leonardo de Moura
284447e43b
chore: style
2020-01-18 18:58:56 -08:00
Leonardo de Moura
53480e077d
feat: ensure tactics invoke synthesizeSyntheticMVars at elabTerm
2020-01-18 18:44:27 -08:00
Leonardo de Moura
1c6d6cccb9
chore: style
2020-01-18 18:27:52 -08:00
Leonardo de Moura
ad72ec4d0d
feat: eval <|> tactic
2020-01-18 18:26:25 -08:00
Leonardo de Moura
c6df6b775b
fix: Tactic.elabTerm must disable errToSorry
2020-01-18 18:25:59 -08:00
Leonardo de Moura
2e6ac0cd61
feat: eval paren tactic
2020-01-18 18:15:27 -08:00
Leonardo de Moura
61d4290fa8
feat: add paren
2020-01-18 18:00:48 -08:00
Leonardo de Moura
66b222879e
feat: eval case tactic
2020-01-18 17:47:43 -08:00
Leonardo de Moura
1bc14d1c62
feat: add List.findM?
2020-01-18 17:42:10 -08:00
Leonardo de Moura
aa84adc0ea
feat: add isSuffixOf
2020-01-18 17:41:58 -08:00
Leonardo de Moura
94a5026790
feat: add goal selection notation
2020-01-18 17:24:19 -08:00
Leonardo de Moura
39dc349167
feat: eval tactic block
2020-01-18 17:22:01 -08:00
Leonardo de Moura
fed91dcbfa
chore: add line break between goals
2020-01-18 16:47:08 -08:00
Leonardo de Moura
e4fca53deb
chore: use getUnsolvedGoals
2020-01-18 16:45:35 -08:00
Leonardo de Moura
9f0b8847de
feat: eval refine
2020-01-18 16:42:27 -08:00
