source
@[export lean_grind_mk_eq_proof]
def Lean.Meta.Grind.mkEqProofImpl (a b : Expr) :
GoalM Expr

Returns a proof that `a = b`. It assumes `a` and `b` are in the same equivalence class.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[export lean_grind_mk_heq_proof]
def Lean.Meta.Grind.mkHEqProofImpl (a b : Expr) :
GoalM Expr
Equations

- Lean.Meta.Grind.mkHEqProofImpl a b = Lean.Meta.Grind.mkEqProofCore✝ a b true

Instances For