Leonardo de Moura
a02421185c
fix: add support for BinderInfo.auxDecl at delabLam
2022-01-10 15:18:49 -08:00
Leonardo de Moura
cee8ad1b66
chore: fix codebase
2022-01-10 15:07:55 -08:00
Leonardo de Moura
4c918a2363
feat: use default_decreasing_tactic at WF/Fix.lean
2022-01-10 14:55:38 -08:00
Leonardo de Moura
739ef7d166
fix: annotate let rec declarations as auxDecl
...
Reason:
1- Tactics such as `assumption` should ignore them.
2- We must annotate recursive applications with `mkRecAppWithSyntax`.
2022-01-10 14:35:05 -08:00
Leonardo de Moura
0dd3ce0598
chore: fix test
2022-01-10 14:31:23 -08:00
Leonardo de Moura
7789779020
feat: add simple default tactic for well-founded recursion
2022-01-10 14:26:08 -08:00
Leonardo de Moura
16b4aa81e5
chore: add helper lemmas for well-founded recursion
2022-01-10 14:07:35 -08:00
Leonardo de Moura
241db0fed6
chore: fix name
2022-01-10 13:20:49 -08:00
Leonardo de Moura
929aafa4c8
fix: generate an error if declaration name clashes with variable name
...
closes #799
2022-01-10 12:08:11 -08:00
Gabriel Ebner
dc65bb080a
fix: race condition in RPC request handler
2022-01-10 13:37:40 +01:00
Sebastian Ullrich
60a70372af
chore: remove stray file breaking stage 0 update
...
/cc @leodemoura
2022-01-10 12:57:51 +01:00
Leonardo de Moura
b2d26380f2
fix: remove auxiliary discriminant let-declarations
2022-01-07 15:03:19 -08:00
Leonardo de Moura
1cf8467847
feat: add unfold conv tactic
2022-01-07 13:51:45 -08:00
Leonardo de Moura
57b9e0852e
fix: clear local context at mkUnfoldEq
2022-01-07 13:51:45 -08:00
Leonardo de Moura
b50e82bc93
feat: unfold tactic
2022-01-07 13:51:45 -08:00
Leonardo de Moura
c303bf6916
refactor: add helper methods for simp
2022-01-07 13:51:45 -08:00
Leonardo de Moura
b1b4705c14
feat: add unfold tactic parsers
2022-01-07 13:51:45 -08:00
Leonardo de Moura
e8a4dbbc2a
chore: document and cleanup mkUnfoldProof
2022-01-07 13:51:45 -08:00
Leonardo de Moura
b797c982fc
feat: add mkUnfoldProof
2022-01-07 13:51:45 -08:00
Gabriel Ebner
f146d456ce
fix: only enable InsertReplaceEdit if supported
2022-01-07 20:28:10 +01:00
larsk21
8c2d7a35d3
fix: make set_option completion replace typed partial name
2022-01-07 17:06:26 +01:00
Mario Carneiro
dcaf3c615f
fix: induction generalizing precedence
2022-01-07 10:45:45 +01:00
Leonardo de Moura
98f4e51a12
feat: add mkUnfoldEq skeleton
2022-01-06 17:42:45 -08:00
Leonardo de Moura
bef161caf7
feat: add better support for discharging equation theorem hypotheses
2022-01-06 14:42:23 -08:00
Leonardo de Moura
df6095e580
fix: casesOnStuckLHS method
...
It was not general enough.
2022-01-06 13:54:17 -08:00
Leonardo de Moura
90b179bea9
fix: add equation theorems even if definition supports smart unfolding
...
See new test.
2022-01-06 13:53:03 -08:00
Leonardo de Moura
d8d7d63830
fix: registers eqns info before adding definition
...
Otherwise `[simp]` at definition will fail to generate equational theorems.
2022-01-06 12:24:40 -08:00
Leonardo de Moura
7acbbb4fbb
fix: auxiliary whnfAux used at mkEqns
2022-01-06 09:57:41 -08:00
Leonardo de Moura
60934bf1d5
feat: add support for removing [simp] attribute from definitions with equational theorems
2022-01-05 16:57:59 -08:00
Leonardo de Moura
c2e52bd577
feat: use getEqnsFor? when applying [simp] at definitions
2022-01-05 15:59:39 -08:00
Leonardo de Moura
ff49fd6b7e
fix: apply afterCompilation attributes after we have compiled *all* definitions in a mutual block
2022-01-05 15:57:51 -08:00
Leonardo de Moura
030e932db8
feat: use getEqnsFor? at simp
2022-01-05 11:28:24 -08:00
Leonardo de Moura
4d1343d670
chore: use _eq instead of eq to name auto generated equational theorems
2022-01-04 17:23:34 -08:00
Leonardo de Moura
b2918e0c76
test: add tests for WF.mkEqns
2022-01-04 17:18:51 -08:00
Leonardo de Moura
d782a97f5c
feat: add WF.mkProof for WF.mkEqns
2022-01-04 17:00:54 -08:00
Leonardo de Moura
2a0cd18d4b
feat: add WF.mkEqns
2022-01-04 15:44:05 -08:00
Leonardo de Moura
d941e97716
feat: add WF/Eqns.lean skeleton
2022-01-04 15:31:22 -08:00
Leonardo de Moura
947240ef9e
refactor: add PreDefinition/Eqns.lean
2022-01-04 13:52:41 -08:00
Mario Carneiro
5a7c9f2d35
chore: add showRhs definition
2022-01-04 09:28:29 -08:00
Mario Carneiro
9ee0d08cb5
chore: add doc
2022-01-04 09:26:34 -08:00
Mario Carneiro
3716e9a2ed
chore: use a different syntax kind for suffices-by
...
chore: update src/Lean/Parser/Term.lean
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-01-04 09:26:32 -08:00
Gabriel Ebner
83e167dfb5
feat: append filename to worker command-line
...
This change has no effect on the server behavior. The only difference
is that the filename now shows up in `htop`, `ps`, etc., which makes it much
easier to see what Lean processes are running, and which are using 100%
CPU, etc.
2022-01-04 15:10:46 +01:00
Sebastian Ullrich
64971a1e3c
fix: term macro errors should be fatal
2022-01-04 11:20:18 +01:00
Leonardo de Moura
b9f7d1defb
fix: constant folding after erasure
...
closes #909
2022-01-03 10:33:07 -08:00
Leonardo de Moura
0e479d1f9f
chore: use double ticks
2022-01-03 10:30:05 -08:00
Leonardo de Moura
e9c112007b
fix: avoid Syntax trees leaks into .olean files
...
closes #918
2022-01-03 09:36:06 -08:00
Mario Carneiro
5e36162f9b
fix: adapt to doHave syntax change
2022-01-03 07:55:52 -08:00
Mario Carneiro
3253231d59
feat: make rw [] syntactically correct
2022-01-03 07:23:24 -08:00
Gabriel Ebner
bc5bd5a671
feat: allow the compiler to optimize unsafeCast
2022-01-03 07:13:55 -08:00
Gabriel Ebner
e605c541d0
fix: do not infer type in erase_irrelevant
...
At the time erase_irrelevant is called, we have already eliminated the
`cast`-applications. Therefore non-atomic expressions may no longer
be well-typed (and `infer_type` can fail).
2022-01-03 07:13:55 -08:00
