Lean4
@[term_elab termCongr, inherit_doc termCongr]
def elabTermCongr : Term.TermElab := fun stx expectedType? => do
match stx with
| `(congr($t)) =>
-- Save the current mvarCounter so that we know which cHoles are for this congr quotation.
let mvarCounterSaved := (← getMCtx).mvarCounter
if let some expectedType := expectedType? then
if let some (expLhsTy, expLhs, expRhsTy, expRhs) := (← whnf expectedType).sides? then
let lhs ← elaboratePattern t expLhsTy true
let rhs ← elaboratePattern t expRhsTy false
unless ← isDefEq expLhs lhs do
throwError "Left-hand side of elaborated pattern{(indentD lhs)}\n\
is not definitionally equal to left-hand side of expected type{indentD expectedType}"
unless ← isDefEq expRhs rhs do
throwError "Right-hand side of elaborated pattern{(indentD rhs)}\n\
is not definitionally equal to right-hand side of expected type{indentD expectedType}"
Term.synthesizeSyntheticMVars (postpone := .yes)
let res ← mkCongrOf 0 mvarCounterSaved lhs rhs
let expectedType' ← whnf expectedType
let pf ←
if expectedType'.iff?.isSome then
res.iff
else if expectedType'.isEq then
res.eq
else if expectedType'.isHEq then
res.heq
else
panic! "unreachable case, sides? guarantees Iff, Eq, and HEq"
return ← mkExpectedTypeHint pf expectedType
let lhs ← elaboratePattern t none true
let rhs ← elaboratePattern t none false
Term.synthesizeSyntheticMVars (postpone := .yes)
let res ← mkCongrOf 0 mvarCounterSaved lhs rhs
let pf ← res.eq
let ty ← mkEq res.lhs res.rhs
mkExpectedTypeHint pf ty
| _ =>
throwUnsupportedSyntax
