Documentation

Lean.Meta.Tactic.Refl

source
def Lean.Meta.refl (mvarId : Lean.MVarId) :
Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.refl.useKernel (lhs : Lean.Expr) (rhs : Lean.Expr) :
Lean.MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.