Documentation

Lean.Elab.PreDefinition.WF.Eqns

Instances For
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.WF.mkEqns (declName : Name) (info : EqnInfo) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.WF.registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) (argsPacker : Meta.ArgsPacker) (hasInduct : Bool) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.