Leonardo de Moura
|
74f732f4cb
|
chore: update stage0
|
2022-01-11 14:45:16 -08:00 |
|
Leonardo de Moura
|
ce76ad44ea
|
feat: add terminationByCore parser
|
2022-01-11 14:44:36 -08:00 |
|
Leonardo de Moura
|
ca89da28d0
|
chore: prepare to rename default_decreasing_tactic
|
2022-01-11 14:42:25 -08:00 |
|
Leonardo de Moura
|
2464da0dca
|
feat: add support for PSigma.Lex at default_decreasing_tactic
|
2022-01-11 14:41:28 -08:00 |
|
Leonardo de Moura
|
a087b21bc0
|
fix: bug at WF/Fix.lean
|
2022-01-11 14:38:31 -08:00 |
|
Leonardo de Moura
|
ec49c31337
|
chore: make sure PSigma.lex signature is similar to Prod.lex
|
2022-01-11 14:37:53 -08:00 |
|
Leonardo de Moura
|
d953ac8d0d
|
feat: allow users to use initialize registerBuiltinDerivingHandler ...
|
2022-01-11 09:50:09 -08:00 |
|
Leonardo de Moura
|
93f3773d83
|
chore: cleanup
|
2022-01-10 16:25:07 -08:00 |
|
Leonardo de Moura
|
dae3489fe2
|
feat: remove partials from Init/Data/Array/Basic.lean
|
2022-01-10 16:05:33 -08:00 |
|
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
|
762b0f42ba
|
chore: fix tests
|
2022-01-10 15:06:03 -08:00 |
|
Leonardo de Moura
|
a28ff92010
|
chore: update stage0
|
2022-01-10 15:05:47 -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
|
57b8912279
|
chore: fix tests
|
2022-01-10 14:33:02 -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 |
|
Josh Levine
|
99f6469761
|
doc: fix typo (#935)
|
2022-01-10 10:26:24 -08:00 |
|
Sebastian Ullrich
|
bcd7185f42
|
chore: CI: try reenabling sanitized Lake test
|
2022-01-10 18:35:22 +01:00 |
|
Sebastian Ullrich
|
768df1581c
|
chore: CI: put llvm-symbolizer in PATH for asan/lsan backtraces
|
2022-01-10 18:35:22 +01:00 |
|
Sebastian Ullrich
|
3acc21e128
|
chore: CI: try to make lsan terminate
|
2022-01-10 18:35:22 +01: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 |
|
Josh Levine
|
1637d75d3f
|
doc: fix trivial typo
|
2022-01-09 10:19:26 +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
|
49d0f3af52
|
test: unfold 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
|
cc4c82a6e7
|
chore: update stage0
|
2022-01-06 17:44:42 -08: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 |
|
Andrei Cheremskoy
|
5eea97534f
|
chore(doc): remove duplicate Tactics section (#927)
|
2022-01-06 14:03:15 -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 |
|