Leonardo de Moura
b91e22af2b
fix: fixes #241
2021-05-22 19:10:07 -07:00
Daniel Fabian
c426a816a1
refactor: Make the non-below version of a premise in the below type for inductive predicates implicit.
...
Since it is always fully implied by the below version thereof, it carries no real information and shouldn't be used in pattern matching.
2021-05-22 18:09:32 -07:00
Leonardo de Moura
28b055463f
fix: fixes #471
2021-05-22 15:42:52 -07:00
Leonardo de Moura
edb203ca54
fix: fixes #481
2021-05-21 20:40:26 -07:00
Leonardo de Moura
795e3a8646
chore: use "theorem" instead of "lemma" in messages
2021-05-21 20:35:23 -07:00
Leonardo de Moura
af4485f40e
fix: fixes #482
2021-05-21 19:20:24 -07:00
Leonardo de Moura
8eceb07caf
feat: new discriminant refinement procedure
2021-05-21 18:08:11 -07:00
Sebastian Ullrich
dd35db610b
feat: server: show final state after tactic combinator
...
No functional change yet because all our combinator have trailing
tactics whose info we prefer
2021-05-21 17:13:33 -07:00
Sebastian Ullrich
4d6c178a6a
refactor: server: actually detect EOF at goalsAt?
2021-05-21 17:13:33 -07:00
Sebastian Ullrich
93327e2324
fix: tactic state on {/·
2021-05-21 17:13:33 -07:00
Leonardo de Moura
73797841ba
feat: add findDiscrRefinementPath
...
The new method is going to be used to improve the discriminant
refinement procedure.
2021-05-20 21:54:48 -07:00
Leonardo de Moura
ed0b008f41
feat: add helper method Term.commitIfNoErrors?
2021-05-20 20:11:12 -07:00
Leonardo de Moura
2646f134d5
chore: add MonadBacktrack instance for ExceptT
2021-05-20 19:24:28 -07:00
Daniel Fabian
42bd44ab82
refactor: Capture environment modification in mkMatcher.
...
Doing this allows us to add the declaration in the backtracking case of structural recursion.
2021-05-20 15:20:16 -07:00
Sebastian Ullrich
9f3ddb0c43
fix: do not store solved goals in info tree
2021-05-20 15:17:54 -07:00
Sebastian Ullrich
a02c6fd3eb
chore: adapt stdlib & tests
2021-05-20 15:17:36 -07:00
Sebastian Ullrich
5b6051b15e
feat: revise have syntax
2021-05-20 15:17:36 -07:00
Sebastian Ullrich
7242c5c513
fix: rw: add all uninstantiated mvars as goals
2021-05-19 07:31:50 -07:00
Daniel Fabian
ab0ef229ac
feat: add getBelowIndices.
2021-05-19 07:28:14 -07:00
Daniel Fabian
91ecbb5b5c
feat: Add withMkMatcherInput.
...
This is the inverse function to `mkMatcher`, i.e. a way to turn a matcher into an input.
2021-05-19 07:28:14 -07:00
Daniel Fabian
cf030a1634
refactor: Add MkMatcherInput.
...
Since we are going to make `mkMatcher` reversible, it's quite useful to have the input be a `structure`. This way we make sure, that the inverse function always returns the same type as `mkMatcher` needs as input.
2021-05-19 07:28:14 -07:00
Sebastian Ullrich
cd5dbc66ce
fix: isolate std streams for all commands in server mode
...
Fixes #475
2021-05-19 13:30:54 +02:00
Sebastian Ullrich
7c3101a51c
chore: produce more efficient/pp-able array code from quotations
2021-05-19 09:52:35 +02:00
Sebastian Ullrich
23f0c1051c
feat: improve ToString/Quote Name
2021-05-19 09:34:01 +02:00
Sebastian Ullrich
3dafe26c72
feat: delab Name.mkStr/Num
2021-05-19 09:21:52 +02:00
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
