Documentation

Lean.Meta.Tactic.Grind.Proof

@[export lean_grind_mk_eq_proof]

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

Equations
    Instances For
      @[export lean_grind_mk_heq_proof]
      Equations
        Instances For