Lean4
/-- If `lhs` or `rhs` is a congruence hole, then process it.
Only process ones that are at least as new as `mvarCounterSaved`
since nothing prevents congruence holes from leaking into the local context. -/
def mkCongrOfCHole? (mvarCounterSaved : Nat) (lhs rhs : Expr) : MetaM (Option CongrResult) := do
match cHole? lhs mvarCounterSaved, cHole? rhs mvarCounterSaved with
| some (isLhs1, val1, pf1), some (isLhs2, val2, pf2) =>
trace[Elab.congr]"mkCongrOfCHole, both holes"
unless isLhs1 == true do
throwCongrEx lhs rhs "A RHS congruence hole leaked into the LHS"
unless isLhs2 == false do
throwCongrEx lhs rhs
"A LHS congruence hole leaked into the RHS"
-- Defeq checks to unify the lhs and rhs congruence holes.
unless ← isDefEq (← inferType pf1) (← inferType pf2) do
throwCongrEx lhs rhs "Elaborated types of congruence holes are not defeq."
if let some (_, lhsVal, _, rhsVal) := (← whnf <| ← inferType pf1).sides? then
unless ← isDefEq val1 lhsVal do
throwError "Left-hand side of congruence hole is{(indentD lhsVal)}\n\
but is expected to be{indentD val1}"
unless ← isDefEq val2 rhsVal do
throwError "Right-hand side of congruence hole is{(indentD rhsVal)}\n\
but is expected to be{indentD val2}"
return some <| CongrResult.mk' val1 val2 pf1
| some .., none =>
throwCongrEx lhs rhs "Right-hand side lost its congruence hole annotation."
| none, some .. =>
throwCongrEx lhs rhs "Left-hand side lost its congruence hole annotation."
| none, none =>
return none
