Leonardo de Moura
|
fc96a24d7b
|
chore: improve error message
|
2021-05-04 19:37:24 -07:00 |
|
Leonardo de Moura
|
dd325cfffc
|
fix: getHeadInfo ==> getHeadInfo?
The generated code was not producing compilation errors because we
have a coercion from `A` to `Option A`
|
2021-05-04 16:46:41 -07:00 |
|
Sebastian Ullrich
|
5b02254297
|
fix: rw final goal state
|
2021-05-04 15:24:42 -07:00 |
|
Sebastian Ullrich
|
aabb4a50aa
|
feat: remove bracket-less rw
|
2021-05-04 15:24:22 -07:00 |
|
Leonardo de Moura
|
2be1595154
|
fix: preserve by toke position information during macro expansion
|
2021-05-04 11:26:34 -07:00 |
|
Leonardo de Moura
|
ac5bb36add
|
fix: save all info nodes during backtracking
|
2021-05-04 11:05:58 -07:00 |
|
Leonardo de Moura
|
91cf32bf88
|
chore: display syntax at tactic info nodes
|
2021-05-04 10:58:54 -07:00 |
|
Sebastian Ullrich
|
c22f4ffaec
|
fix: partial fix of focus goal state
|
2021-05-04 19:11:05 +02:00 |
|
Leonardo de Moura
|
8102f407b6
|
fix: take binder information into account when caching results
|
2021-05-03 21:02:23 -07:00 |
|
Leonardo de Moura
|
1279063e0d
|
fix: fixes #248
|
2021-05-03 18:20:36 -07:00 |
|
Leonardo de Moura
|
e8aa02cd51
|
feat: closes #415
|
2021-05-03 18:04:01 -07:00 |
|
Leonardo de Moura
|
1e41e2eb4a
|
chore: use double backticks
|
2021-05-03 14:26:27 -07:00 |
|
Leonardo de Moura
|
a5c28f7dfc
|
fix: fixes #243
|
2021-05-03 13:01:16 -07:00 |
|
Leonardo de Moura
|
eaa7582e60
|
feat: add toPattern
|
2021-05-03 11:44:40 -07:00 |
|
Leonardo de Moura
|
6efb058e2c
|
refactor: add Name.modifyBase
|
2021-05-03 10:06:20 -07:00 |
|
Sebastian Ullrich
|
e76fc17b0e
|
fix: rw goal state positions
|
2021-05-03 14:14:12 +02:00 |
|
Sebastian Ullrich
|
4fb01f7c06
|
fix: goal state on ;
|
2021-05-03 13:32:00 +02:00 |
|
Sebastian Ullrich
|
8420a33626
|
fix: do not leak nested definitions from example
|
2021-05-03 09:11:14 +02:00 |
|
Leonardo de Moura
|
e5083f2521
|
fix: avoid unnecessary unfolding at do
|
2021-05-02 21:29:32 -07:00 |
|
Leonardo de Moura
|
cadaecb40a
|
fix: similar to previous commit but for LevelMVarToParam
|
2021-05-02 19:54:52 -07:00 |
|
Leonardo de Moura
|
506bfb8d0b
|
fix: take binder information into account when caching results at instantiateMVars
|
2021-05-02 19:40:58 -07:00 |
|
Leonardo de Moura
|
56c7454a8d
|
fix: fixes #435
|
2021-05-02 18:16:57 -07:00 |
|
Leonardo de Moura
|
0f8c6ca797
|
fix: cache issue at instantiateBetaRevRange
|
2021-05-02 17:00:35 -07:00 |
|
Leonardo de Moura
|
78a2de4241
|
feat: better error recovery for match syntax
|
2021-05-02 17:00:35 -07:00 |
|
Leonardo de Moura
|
59b1f8c143
|
chore: avoid match_syntax in error messages
|
2021-05-02 17:00:35 -07:00 |
|
Sebastian Ullrich
|
b8b8cc79a9
|
feat: show initial case goal on ... => for induction/cases/case/match
|
2021-05-02 23:07:15 +02:00 |
|
Sebastian Ullrich
|
8863761401
|
feat: show initial state for tactic combinators by default
|
2021-05-02 23:07:15 +02:00 |
|
Sebastian Ullrich
|
2734a5baba
|
feat: show state on by
|
2021-05-02 23:07:15 +02:00 |
|
Leonardo de Moura
|
1a0fc816b1
|
feat: rename inaccessible variable names at cases
|
2021-05-01 21:51:58 -07:00 |
|
Leonardo de Moura
|
663a5124f4
|
chore: naming convention
|
2021-05-01 21:29:06 -07:00 |
|
Leonardo de Moura
|
93189e0fce
|
chore: prepare to change case tactic
|
2021-05-01 19:53:44 -07:00 |
|
Leonardo de Moura
|
9d934694e7
|
feat: refine binop% elaborator
see issue #382
|
2021-04-30 19:37:58 -07:00 |
|
Leonardo de Moura
|
d01fb5451c
|
feat: add support for binop% at elabCDotFunctionAlias
|
2021-04-30 19:17:16 -07:00 |
|
Leonardo de Moura
|
0a018f2369
|
chore: add support for binop% in patterns
|
2021-04-30 18:38:44 -07:00 |
|
Leonardo de Moura
|
f22fd49ae2
|
feat: add binop% elaborator
This is an experiment, we will probably need to tweak its behavior.
See issue #382
|
2021-04-30 18:21:21 -07:00 |
|
Leonardo de Moura
|
f8ac5d25dd
|
feat: add notation for helper elaboration function
This similar to `binrel%` but for binary operators.
See issue #382
|
2021-04-30 17:14:17 -07:00 |
|
Sebastian Ullrich
|
e1cde87c43
|
fix: server: completion & goal state at EOF
|
2021-04-30 19:25:53 +02:00 |
|
tydeu
|
44f45f426c
|
feat: add scoped macro_rules (#432)
|
2021-04-30 09:05:09 +02:00 |
|
Leonardo de Moura
|
adae6fdb40
|
fix: tolerate type incorrect terms
This bug was producing a type error when I was using `set_option trace.Elab true`
|
2021-04-29 21:34:15 -07:00 |
|
Daniel Fabian
|
d54c964a51
|
fix: improve the tactic for brecOn for inductive predicates.
|
2021-04-29 17:19:09 -07:00 |
|
Sebastian Ullrich
|
f0960b7f89
|
fix: ignore antiquotations outside quotations
|
2021-04-29 13:33:48 +02:00 |
|
Sebastian Ullrich
|
73cf3533a1
|
fix: count quotation depth in parser correctly
|
2021-04-29 13:33:48 +02:00 |
|
Sebastian Ullrich
|
7990f6e6e1
|
perf: use optimized withAntiquot in leading_parser
|
2021-04-29 13:30:09 +02:00 |
|
Sebastian Ullrich
|
683ecb2d65
|
feat: ignore unquoted identifiers in prechecked quotations
|
2021-04-29 13:30:09 +02:00 |
|
Leonardo de Moura
|
45bcf4a32c
|
feat: check instance implicit binder annotations
|
2021-04-28 17:15:08 -07:00 |
|
Sebastian Ullrich
|
40b17bc364
|
refactor: introduce a few double-backtick quotations
|
2021-04-28 12:09:13 +02:00 |
|
Sebastian Ullrich
|
75e95f93a9
|
feat: improve let error locality
|
2021-04-27 16:38:46 -07:00 |
|
Sebastian Ullrich
|
9f0fa19237
|
feat: notation: unfold to prechecked quotation
|
2021-04-27 16:38:37 -07:00 |
|
Sebastian Ullrich
|
ad7ee2c81b
|
fix: disable quotation precheck if hygiene is false
|
2021-04-27 16:38:37 -07:00 |
|
Sebastian Ullrich
|
9301e05a7e
|
feat: double-quoted quotation semantics and basic precheck hooks
|
2021-04-27 16:38:37 -07:00 |
|