From 9c293abb9cb0d31e978d026ca68970271a78a853 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 25 Jan 2022 18:19:36 -0800 Subject: [PATCH] chore: expose `heqToEq` tactic --- src/Lean/Meta/Tactic/Injection.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean index b1965b0ec5..b6310ba5c0 100644 --- a/src/Lean/Meta/Tactic/Injection.lean +++ b/src/Lean/Meta/Tactic/Injection.lean @@ -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