max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: expose heqToEq tactic

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-25 18:19:36 -08:00
parent 6547af988b
commit 9c293abb9c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Injection.lean
View file

@ -62,7 +62,7 @@ inductive InjectionResult where
| solved
| subgoal (mvarId : MVarId) (newEqs : Array FVarId) (remainingNames : List Name)
private def heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool) : MetaM (FVarId × MVarId) :=
def heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool) : MetaM (FVarId × MVarId) :=
withMVarContext mvarId do
let decl ← getLocalDecl fvarId
let type ← whnf decl.type