From 9c40a839563ce5ae2235469ca473208668f5aa20 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 3 Sep 2024 19:05:16 -0700 Subject: [PATCH] fix: Instantiate type when detecting `eq` --- Pantograph/Tactic/Congruence.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean index dfb329d..f72fc0a 100644 --- a/Pantograph/Tactic/Congruence.lean +++ b/Pantograph/Tactic/Congruence.lean @@ -7,7 +7,7 @@ namespace Pantograph.Tactic def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg let target ← mvarId.getType - let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq" + let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq" let userName := (← mvarId.getDecl).userName let u ← Meta.mkFreshLevelMVar @@ -36,7 +36,7 @@ def evalCongruenceArg: Elab.Tactic.TacticM Unit := do def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun let target ← mvarId.getType - let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq" + let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq" let userName := (← mvarId.getDecl).userName let u ← Meta.mkFreshLevelMVar let α ← Meta.mkFreshExprMVar (.some $ mkSort u) @@ -65,7 +65,7 @@ def evalCongruenceFun: Elab.Tactic.TacticM Unit := do def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do mvarId.checkNotAssigned `Pantograph.Tactic.congruence let target ← mvarId.getType - let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq" + let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq" let userName := (← mvarId.getDecl).userName let u ← Meta.mkFreshLevelMVar let α ← Meta.mkFreshExprMVar (.some $ mkSort u)