max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
26800 commits 1 branch 0 tags 5.3 GiB
Commit graph

3889 commits

Author SHA1 Message Date
Joscha
fead5526bc feat: add -i cli option 2022-01-14 09:18:57 +01:00
Leonardo de Moura
6d235586f0 fix: ignore TC failures while processing patterns 
closes #948
 2022-01-13 10:55:09 -08:00
Leonardo de Moura
1620987b6c fix: recursive applications in discriminants 2022-01-13 09:56:33 -08:00
Leonardo de Moura
9162901c86 fix: expandTerminationByNonCore 2022-01-12 16:22:54 -08:00
Leonardo de Moura
91a0ac8a12 feat: elaborate new termination_by syntax 2022-01-12 16:15:30 -08:00
Leonardo de Moura
49b2860f2a feat: add Meta.rename tactic 2022-01-12 16:15:30 -08:00
Leonardo de Moura
addcbc6fa3 feat: process termination_by syntax 2022-01-12 16:15:30 -08:00
Leonardo de Moura
111d09fda3 fix: must apply afterCompilation attributes *after* smart unfolding definition was declared 
The `[simp]` attribute checks whether the smart unfolding defintion
has been declared.

closes #946
 2022-01-12 08:28:03 -08:00
Leonardo de Moura
e7eab602d9 fix: missing consumeAutoOptParam at addNewArg 2022-01-12 08:28:03 -08:00
Leonardo de Moura
7a86b613dc chore: remove old comment 2022-01-12 08:28:03 -08:00
Leonardo de Moura
a1ab5c0ccb feat: simplify termination_by new syntax 
We don't need `using` anymore since we are going to use TC inference.
 2022-01-12 08:28:03 -08:00
Gabriel Ebner
50abc3e295 fix: correctly pretty-print @Eq 2022-01-12 09:41:41 +01:00
Gabriel Ebner
bdc80ce50d fix: potential nontermination in delabFor 2022-01-12 09:41:41 +01:00
Gabriel Ebner
9132b27e80 fix: delabAppImplicit: strip mdata from function 2022-01-12 09:41:41 +01:00
Leonardo de Moura
de19767594 feat: basic skeleton for termination_by' vs termination_by 2022-01-11 16:53:39 -08:00
Leonardo de Moura
868a43a747 chore: remove dead code 2022-01-11 16:22:20 -08:00
Leonardo de Moura
f9b79092f6 feat: new termination_by syntax 2022-01-11 15:36:50 -08:00
Leonardo de Moura
430b641e81 feat: use decreasing_tactic 2022-01-11 14:47:19 -08:00
Leonardo de Moura
ce76ad44ea feat: add terminationByCore parser 2022-01-11 14:44:36 -08:00
Leonardo de Moura
a087b21bc0 fix: bug at WF/Fix.lean 2022-01-11 14:38:31 -08:00
Leonardo de Moura
d953ac8d0d feat: allow users to use initialize registerBuiltinDerivingHandler ... 2022-01-11 09:50:09 -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
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
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
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
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