Leonardo de Moura
|
d15f3431dc
|
feat: add #check_failure command
|
2020-02-12 11:28:44 -08:00 |
|
Leonardo de Moura
|
9221a9d349
|
fix: typo at consumeLet
|
2020-02-12 10:17:30 -08:00 |
|
Leonardo de Moura
|
6429486f88
|
refactor: decouple elaboration for forall and lambda binders
Motivation: another refactoring to improve `elabFunCore`.
|
2020-02-12 09:11:20 -08:00 |
|
Leonardo de Moura
|
fae52a7ba6
|
fix: @($f:fun) case
|
2020-02-12 08:46:25 -08:00 |
|
Leonardo de Moura
|
f0e3cf449f
|
fix: unhygienic method
|
2020-02-11 21:15:05 -08:00 |
|
Leonardo de Moura
|
61e57318eb
|
fix: assigning a delayed assigned metavar
|
2020-02-11 21:03:24 -08:00 |
|
Leonardo de Moura
|
41baf46083
|
feat: propagate expected type at elabFunCore
|
2020-02-11 17:47:51 -08:00 |
|
Leonardo de Moura
|
abd0f54ce6
|
chore: minor reorg before improving elabFunCore
|
2020-02-11 17:20:20 -08:00 |
|
Leonardo de Moura
|
5e400dfe57
|
feat: use isTypeFormer
|
2020-02-11 16:13:41 -08:00 |
|
Leonardo de Moura
|
2f959e23ca
|
fix: checkAssignment was overwriting assignment
|
2020-02-11 16:11:56 -08:00 |
|
Leonardo de Moura
|
55231b960e
|
feat: simplify and improve processAssignmentFOApproxAux
|
2020-02-11 14:42:02 -08:00 |
|
Leonardo de Moura
|
30e0ccd8c4
|
feat: implicit lambdas
It is still work in progress
|
2020-02-11 13:43:05 -08:00 |
|
Leonardo de Moura
|
8044682b34
|
fix: type class instance arguments _ at explicit applications @f _ _
|
2020-02-11 13:36:52 -08:00 |
|
Leonardo de Moura
|
03b5b7d562
|
feat: implicit lambdas
|
2020-02-11 09:59:46 -08:00 |
|
Leonardo de Moura
|
4f91e0b0d9
|
feat: propagate before final ensureHasType
|
2020-02-11 09:59:23 -08:00 |
|
Leonardo de Moura
|
ae8eab42ca
|
feat: update @ elaborator
|
2020-02-11 09:35:37 -08:00 |
|
Leonardo de Moura
|
a276b59a80
|
feat: allow arbitrary terms after @
|
2020-02-11 08:59:17 -08:00 |
|
Leonardo de Moura
|
7085072590
|
feat: allow implicitBinder and instBinder at fun
|
2020-02-11 08:26:10 -08:00 |
|
Leonardo de Moura
|
f6ae8560e8
|
fix: isDefEq issue exposed by new test
|
2020-02-10 23:46:17 -08:00 |
|
Leonardo de Moura
|
e732eac899
|
fix: but at elimMVarDepsApp
|
2020-02-10 20:49:43 -08:00 |
|
Leonardo de Moura
|
c635f2cc8f
|
chore: remove dead code
|
2020-02-10 20:04:43 -08:00 |
|
Leonardo de Moura
|
d29e15df65
|
refactor: reorganize code for new feature
|
2020-02-10 19:10:26 -08:00 |
|
Leonardo de Moura
|
97057e56e0
|
feat: add isTypeFormer
|
2020-02-10 19:06:34 -08:00 |
|
Leonardo de Moura
|
05fcb9b4d4
|
chore: remove MonadFail
|
2020-02-10 13:54:27 -08:00 |
|
Leonardo de Moura
|
55763da0ab
|
chore: cleanup
|
2020-02-10 12:38:35 -08:00 |
|
Leonardo de Moura
|
11d75addf3
|
feat: add helper tactics
|
2020-02-10 12:17:29 -08:00 |
|
Leonardo de Moura
|
9017ddf1f1
|
chore: remove [inline] to control code blow up
|
2020-02-09 19:31:11 -08:00 |
|
Leonardo de Moura
|
c3b2a1da50
|
fix: bug at subst tactic
|
2020-02-09 19:25:15 -08:00 |
|
Leonardo de Moura
|
472ae6adac
|
fix: typos and bugs
|
2020-02-09 19:12:01 -08:00 |
|
Leonardo de Moura
|
4d20fc8b5a
|
fix: preserveOrder logic
|
2020-02-09 19:01:12 -08:00 |
|
Leonardo de Moura
|
8d97b7c72e
|
chore: missing ,
|
2020-02-09 19:00:56 -08:00 |
|
Leonardo de Moura
|
55074b2a17
|
feat: add subst tactic
|
2020-02-09 18:42:06 -08:00 |
|
Leonardo de Moura
|
15554e7ce0
|
feat: add useUnusedNames option
|
2020-02-09 18:04:48 -08:00 |
|
Leonardo de Moura
|
36a15fbc5b
|
fix: propagate tag at revert
|
2020-02-09 18:04:28 -08:00 |
|
Leonardo de Moura
|
405ee2dcb7
|
feat: add FVarSubst
|
2020-02-09 17:34:29 -08:00 |
|
Leonardo de Moura
|
3c235c3613
|
chore: naming convention
|
2020-02-09 17:10:20 -08:00 |
|
Leonardo de Moura
|
a4a3f7d6a5
|
fix: typo
|
2020-02-09 16:47:14 -08:00 |
|
Leonardo de Moura
|
22ff3c7db2
|
feat: add evalClear
|
2020-02-09 16:41:29 -08:00 |
|
Leonardo de Moura
|
164cd4395a
|
refactor: improve dependsOn API
|
2020-02-09 16:27:37 -08:00 |
|
Leonardo de Moura
|
b977fb8887
|
chore: add clear and subst parsers
|
2020-02-09 11:31:24 -08:00 |
|
Leonardo de Moura
|
fcca8a2a67
|
feat: add clear tactic
|
2020-02-09 11:29:46 -08:00 |
|
Leonardo de Moura
|
95ad26cc23
|
feat: add mkEqNDRec and mkEqRec
|
2020-02-09 11:02:35 -08:00 |
|
Leonardo de Moura
|
d8b69d4fe1
|
feat: better error messages at MetaHasEval
|
2020-02-09 10:49:07 -08:00 |
|
Leonardo de Moura
|
277dbd00cb
|
feat: add preserveOrder flag
|
2020-02-09 09:36:27 -08:00 |
|
Leonardo de Moura
|
0092c40ce4
|
refactor: make it clear the result are free variables
|
2020-02-09 08:38:37 -08:00 |
|
Leonardo de Moura
|
7c7c4edf38
|
feat: add evalRevert
|
2020-02-08 18:51:11 -08:00 |
|
Leonardo de Moura
|
e54c803219
|
chore: add relaxed option
|
2020-02-08 18:50:30 -08:00 |
|
Leonardo de Moura
|
029611b097
|
chore: missing change
|
2020-02-08 18:50:18 -08:00 |
|
Leonardo de Moura
|
da2e5b6fdf
|
fix: must set mvar as natural
|
2020-02-08 18:49:33 -08:00 |
|
Leonardo de Moura
|
7a556d8f61
|
fix: use metavariable local context
|
2020-02-08 18:48:08 -08:00 |
|