Leonardo de Moura
164b26bf01
fix: make sure the resulting array size is equal to the number of binders
...
The following code relies on this property
```lean
for uid in scope.varUIds, x in xs do
sectionFVars := sectionFVars.insert uid x
```
2021-05-04 19:46:14 -07:00
Leonardo de Moura
fc96a24d7b
chore: improve error message
2021-05-04 19:37:24 -07:00
Leonardo de Moura
7398db5f3f
fix: rw final goal state
2021-05-04 16:58:44 -07:00
Leonardo de Moura
56d5d6c564
chore: fix tests
2021-05-04 15:42:03 -07:00
Sebastian Ullrich
aabb4a50aa
feat: remove bracket-less rw
2021-05-04 15:24:22 -07:00
Leonardo de Moura
88a2f43d73
chore: fix test output
2021-05-04 11:30:11 -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
a5c28f7dfc
fix: fixes #243
2021-05-03 13:01:16 -07:00
Leonardo de Moura
061709aa51
refactor: use Lean version
...
This commit also fixes a problem reported by Marc.
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
Leonardo de Moura
e5083f2521
fix: avoid unnecessary unfolding at do
2021-05-02 21:29:32 -07:00
Leonardo de Moura
d556ebbdc6
test: add test for binder caching issue
2021-05-02 20:04:41 -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
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
a2e8bc0780
feat: use binop% to define arith operators
...
closes #382
2021-04-30 19:40:45 -07:00
Leonardo de Moura
a04babf263
chore: fix tests affected by recent changes
2021-04-30 19:37:18 -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
Sebastian Ullrich
f0960b7f89
fix: ignore antiquotations outside quotations
2021-04-29 13:33:48 +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
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
9301e05a7e
feat: double-quoted quotation semantics and basic precheck hooks
2021-04-27 16:38:37 -07:00
Leonardo de Moura
35411d5b2c
chore: fix tests
2021-04-27 16:06:26 -07:00
Daniel Fabian
0238bf8c33
refactor: use Ordering inside of rbmap instead of lt.
2021-04-27 07:58:58 -07:00
Leonardo de Moura
18085b9712
fix: improve match generalizing feature
2021-04-26 19:22:03 -07:00
Daniel Fabian
1f05f5bf11
chore: rename ProofBelow to below.
2021-04-26 20:33:21 +02:00
Sebastian Ullrich
14c5ec559b
test: forgot tabs ban test
2021-04-26 17:09:48 +02:00
Leonardo de Moura
af391fe812
test: reflective inductive predicate
2021-04-25 20:35:13 -07:00
Daniel Fabian
eda4bdd337
test: extend inductive_pred.lean with tests using the new construction.
2021-04-25 20:02:22 -07:00
Leonardo de Moura
2cbdd637c7
test: add second example for issue #423
2021-04-25 10:35:23 -07:00
Leonardo de Moura
b670d6b8d7
test: for issue #423
2021-04-25 10:30:26 -07:00
Leonardo de Moura
0533fc4056
chore: fix test
2021-04-25 10:25:35 -07:00
Leonardo de Moura
f47f605039
fix: remove incorrect test
...
It had two problems:
- It was preventing coercions from being applied.
- It was compromising error recovery. The body of the lambda was not
being elaborated when the exception was thrown.
The new error message is more verbose and potentially confusing, but
it is better than the one produced this morning.
2021-04-24 22:17:29 -07:00
Leonardo de Moura
1f9975d35d
feat: improve error message and include variables introduced by the implicit lambda notation
2021-04-24 21:34:42 -07:00
Leonardo de Moura
10185d24dd
feat: improve error message
2021-04-24 20:43:13 -07:00
