Leonardo de Moura
|
b0f0a59729
|
refactor: elabDiscrs
Elaborate discriminants forward and infer match-type backwards.
|
2021-05-18 19:59:11 -07:00 |
|
Leonardo de Moura
|
8f5c39e2b8
|
chore: fix typo
|
2021-05-18 19:35:55 -07:00 |
|
Leonardo de Moura
|
96ed029308
|
refactor: use StateRefT at elabDiscrs
|
2021-05-18 19:29:25 -07:00 |
|
Leonardo de Moura
|
7cabbc814d
|
chore: cleanup before extending match
|
2021-05-18 18:29:23 -07:00 |
|
Leonardo de Moura
|
eae1f5412b
|
fix: bugs introduced in the previous commits
|
2021-05-17 15:00:51 -07:00 |
|
Leonardo de Moura
|
a3e09a983f
|
chore: remove leftovers
|
2021-05-17 14:47:04 -07:00 |
|
Leonardo de Moura
|
3b7bcdc449
|
feat: add endPos field to SourceInfo.original
We need an update stage0 before we use it.
|
2021-05-17 14:32:58 -07:00 |
|
Sebastian Ullrich
|
eb93894683
|
fix: do not abort elaboration on unclosed parenthesis
|
2021-05-17 22:29:06 +02:00 |
|
Leonardo de Moura
|
53b2ceea51
|
fix: missing withoutModifyingState at elabSimpConfig
|
2021-05-16 13:07:13 -07:00 |
|
Leonardo de Moura
|
62ee8cfcea
|
feat: add MonadBacktrack instance for SimpM
|
2021-05-16 12:49:33 -07:00 |
|
Leonardo de Moura
|
ac90052139
|
feat: add option for controlling how deep we go when trying to discharge simp theorem hypotheses
|
2021-05-16 12:32:05 -07:00 |
|
Leonardo de Moura
|
50cf4216ac
|
feat: closes #440
|
2021-05-15 20:54:54 -07:00 |
|
Leonardo de Moura
|
37c1608ec3
|
feat: improve error handling in tactic blocks
|
2021-05-15 20:18:48 -07:00 |
|
Leonardo de Moura
|
4b69193442
|
feat: generalize withPPInaccessibleNames
|
2021-05-15 18:58:06 -07:00 |
|
Leonardo de Moura
|
dbe0d2d706
|
feat: automatically generate injectivity theorems
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
051ac3aef3
|
fix: casesRec
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
0f43a338e6
|
feat: improve error message
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
05147fd352
|
fix: do not generate injectivity theorems for unsafe inductive datatypes
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
175311b2f0
|
feat: avoid trivial injectivity theorems
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
112bb0ed79
|
fix: injectivity theorem for constructors with dependent fields
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
2a7ec9dd8c
|
feat: add splitAnd and applyRefl helper methods
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
77b9dbf9a9
|
feat: add casesRec
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
eb4df90c93
|
feat: add helper methods
|
2021-05-14 18:05:04 -07:00 |
|
Sebastian Ullrich
|
7ca2f70c2f
|
feat: Eq.rec delaborator
|
2021-05-14 18:36:59 +02:00 |
|
Sebastian Ullrich
|
3f9c015dd4
|
feat: pp.proofs & pp.proofs.withType
Resolves #210
|
2021-05-14 15:14:58 +02:00 |
|
Sebastian Ullrich
|
7ec262af66
|
feat: Eq.ndrec delaborator
|
2021-05-14 14:59:47 +02:00 |
|
Sebastian Ullrich
|
6a03e15a79
|
feat: watchdog: show message while worker is starting
|
2021-05-14 14:59:47 +02:00 |
|
Leonardo de Moura
|
bf583f6065
|
chore: add placeholders for mkInjectiveTheorems
We can activate them yet since the method is failing when there are
heterogeous equalities in the injectivity theorem type.
|
2021-05-13 22:36:45 -07:00 |
|
Leonardo de Moura
|
6a45799244
|
feat: elaborate bootstrapping helper command gen_injective_theorems%
|
2021-05-13 22:27:05 -07:00 |
|
Leonardo de Moura
|
71cd067e94
|
feat: add helper command
|
2021-05-13 22:10:35 -07:00 |
|
Leonardo de Moura
|
f850820029
|
feat: add mkInjectiveTheorems
|
2021-05-13 22:09:50 -07:00 |
|
Leonardo de Moura
|
ea45d3bd40
|
fix: fixes #457
|
2021-05-12 20:45:54 -07:00 |
|
Leonardo de Moura
|
4db3ccaddb
|
feat: type ascription should disable implicit lambdas
|
2021-05-12 19:29:36 -07:00 |
|
Sebastian Ullrich
|
8ae726203d
|
fix: plainGoal: consider original positions only when deciding whether a tactic is a combinator
|
2021-05-12 10:51:42 +02:00 |
|
Leonardo de Moura
|
c9db8619f1
|
fix: fixes #456
|
2021-05-11 21:07:21 -07:00 |
|
Sebastian Ullrich
|
1e6dadfa52
|
fix: documentHighlight on partial input
Fixes #455
|
2021-05-11 17:03:18 +02:00 |
|
Leonardo de Moura
|
b52edf1259
|
fix: fixes #452
The new syntax is similar to `matchAlts` and uses `colGe`.
The first `|` is not optional anymore.
|
2021-05-10 17:28:10 -07:00 |
|
Leonardo de Moura
|
7d39a0d56c
|
chore: prepare to change first syntax
|
2021-05-10 17:05:31 -07:00 |
|
Leonardo de Moura
|
0e1f645b07
|
fix: fixes #450
|
2021-05-10 13:55:06 -07:00 |
|
Leonardo de Moura
|
e49dfccc2a
|
chore: remove dead variable
|
2021-05-10 13:41:55 -07:00 |
|
Leonardo de Moura
|
2a676b6dfb
|
fix: fixes #449
|
2021-05-10 13:10:59 -07:00 |
|
Leonardo de Moura
|
89373bd64f
|
fix: fixes #447
|
2021-05-08 19:04:12 -07:00 |
|
Leonardo de Moura
|
4675817a9e
|
fix: projection of string literals
|
2021-05-07 14:38:21 -07:00 |
|
Leonardo de Moura
|
5fcd08326f
|
fix: bug at reduceRec
|
2021-05-07 14:21:37 -07:00 |
|
Sebastian Ullrich
|
05b12e2b61
|
chore: undo workaround
|
2021-05-07 16:09:42 +02:00 |
|
Sebastian Ullrich
|
088774536e
|
fix: syntax match: do not discard other patterns after splices
|
2021-05-07 16:08:10 +02:00 |
|
Sebastian Ullrich
|
6f9b80d91c
|
fix: parenthesizer: avoid panic on partial syntax trees
Fixes #446
|
2021-05-07 09:42:14 +02:00 |
|
Leonardo de Moura
|
475f5fecaa
|
feat: improve error recovery at Tactic.elabTerm
|
2021-05-06 20:44:36 -07:00 |
|
Leonardo de Moura
|
8e81f03e3a
|
chore: adjust stdlib to recent changes
|
2021-05-06 15:43:56 -07:00 |
|
Leonardo de Moura
|
7fc6607611
|
feat: have ... := ... syntax closer to let
|
2021-05-06 15:38:57 -07:00 |
|