HepLean Documentation

Lean.Elab.PreDefinition.Nonrec.Eqns

source
def Lean.Elab.Nonrec.mkEqns (declName : Lake.Name) (info : Lean.DefinitionVal) :
Lean.MetaM (Array Lake.Name)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Nonrec.getEqnsFor? (declName : Lake.Name) :
    Lean.MetaM (Option (Array Lake.Name))
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For