pushSubsingletonEq — Mathlib

Lean4
/-- Given subsingleton elements `a` and `b` which are not necessarily of the same type, if the
types of `a` and `b` are equivalent, add the (heterogeneous) equality proof between `a` and `b` to
the todo list. -/
def pushSubsingletonEq (a b : Expr) : CCM Unit := do
  -- Remark: we must normalize here because we have to do so before
    -- internalizing the types of `a` and `b`.

  let A ← normalize (← inferType a)
  let B ←
    normalize
        (← inferType b)
          -- TODO(Leo): check if the following test is a performance bottleneck

  if ← pureIsDefEq A B then
    let proof ← mkAppM ``FastSubsingleton.elim #[a, b]
    pushEq a b proof
  else
    let some AEqB ← getEqProof A B |
      failure
    let proof ← mkAppM ``FastSubsingleton.helim #[AEqB, a, b]
    pushHEq a b proof
Похожие утверждения