aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

fix: Instantiate type when detecting eq #91

Merged
aniva merged 1 commits from bug/eq-detection-in-congruence into dev 2024-09-03 19:19:10 -07:00
Conversation 0 Commits 1 Files Changed 1 +3 -3
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Pantograph/Tactic/Congruence.lean
View File

@ -7,7 +7,7 @@ namespace Pantograph.Tactic
def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg
let target ← mvarId.getType 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 userName := (← mvarId.getDecl).userName
let u ← Meta.mkFreshLevelMVar 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 def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
let target ← mvarId.getType 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 userName := (← mvarId.getDecl).userName
let u ← Meta.mkFreshLevelMVar let u ← Meta.mkFreshLevelMVar
let α ← Meta.mkFreshExprMVar (.some $ mkSort u) 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 def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.congruence mvarId.checkNotAssigned `Pantograph.Tactic.congruence
let target ← mvarId.getType 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 userName := (← mvarId.getDecl).userName
let u ← Meta.mkFreshLevelMVar let u ← Meta.mkFreshLevelMVar
let α ← Meta.mkFreshExprMVar (.some $ mkSort u) let α ← Meta.mkFreshExprMVar (.some $ mkSort u)