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`

This commit is contained in:
Leni Aniva 2024-09-03 19:05:16 -07:00
parent f8df2599f9
commit 9c40a83956
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
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)