max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta/Tactic
History
Leonardo de Moura e574c5373f feat: improve delta? method 
Use zeta reduction to create new opportunities of beta-reduction.

This issue fixes on the problems that were affecting the generation of
equation theorems for `Array.heapSort.loop` (see issue: #998).
After this fix, the equation theorem generation fails at `splitMatch`.
2022-02-09 13:31:55 -08:00
..
Simp feat: add simpTargetStar 2022-02-08 11:43:45 -08:00
Apply.lean refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files 2021-12-06 09:57:00 -08:00
Assert.lean fix: location notation and simp 2021-03-19 19:54:22 -07:00
Assumption.lean refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files 2021-12-06 09:57:00 -08:00
AuxLemma.lean chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Cases.lean feat: add throwNestedTacticEx 2022-01-31 16:25:44 -08:00
Cleanup.lean fix: avoid getMVarType' at cleanup tactic 2021-10-19 06:43:07 -07:00
Clear.lean chore: cleanup 2022-01-26 09:18:17 -08:00
Constructor.lean feat: add constructor tactic 2021-05-06 10:40:56 -07:00
Contradiction.lean feat: improve contradiction 2022-02-08 13:26:05 -08:00
Delta.lean feat: improve delta? method 2022-02-09 13:31:55 -08:00
ElimInfo.lean fix: leftovers in the local context when applying induction 2021-03-27 19:42:22 -07:00
FVarSubst.lean chore: use deriving Inhabited 2020-12-13 11:57:59 -08:00
Generalize.lean feat: nary generalize tactic 2021-08-30 16:31:39 -07:00
Induction.lean fix: induction MetaM tactic 2022-01-31 13:41:38 -08:00
Injection.lean chore: expose heqToEq tactic 2022-01-25 18:43:51 -08:00
Intro.lean refactor: avoid Name, MVarId, and FVarId confusion 2021-09-07 19:06:50 -07:00
Rename.lean feat: add Meta.rename tactic 2022-01-12 16:15:30 -08:00
Replace.lean feat: add replaceLocalDeclDefEq 2021-09-09 13:07:33 -07:00
Revert.lean fix: fixes #310 2021-02-12 18:14:42 -08:00
Rewrite.lean feat: add Meta.Rewrite.Config 2021-09-12 18:44:08 -07:00
Simp.lean refactor: CongrLemma => SimpCongrTheorem 2022-02-06 09:15:39 -08:00
Split.lean chore: "simp lemma" => "simp theorem" 2022-02-06 09:15:39 -08:00
SplitIf.lean chore: "simp lemma" => "simp theorem" 2022-02-06 09:15:39 -08:00
Subst.lean feat: add substVars 2022-01-25 18:43:51 -08:00
Unfold.lean chore: "simp lemma" => "simp theorem" 2022-02-06 09:15:39 -08:00
Util.lean feat: add simpTargetStar 2022-02-08 11:43:45 -08:00