fix: Instantiate type when detecting eq
#91
|
@ -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)
|
||||||
|
|
Loading…
Reference in New Issue