Lean4
/-- Elaborates a congruence hole and returns either the left-hand side or the right-hand side,
annotated with information necessary to generate a congruence lemma. -/
def elabCHole (h : Syntax) (forLhs : Bool) (expectedType? : Option Expr) : Term.TermElabM Expr := do
let pf ← Term.elabTerm h none
let pfTy ← inferType pf
unless ← isDefEq (← inferType pfTy) (.sort .zero) do
throwError "Hole has type{indentD pfTy}\nbut is expected to be a Prop"
if let some (_, lhs, _, rhs) := (← whnf pfTy).sides? then
let val := if forLhs then lhs else rhs
if let some expectedType := expectedType? then
-- Propagate type hint:
discard <| isDefEq expectedType (← inferType val)
mkCHole forLhs val pf
else
-- Since `pf` doesn't yet have sides, we resort to the value and the proof being decoupled.
-- These will be unified during congruence generation.
mkCHole forLhs (← mkFreshExprMVar expectedType?) pf
