Documentation

Lean.Elab.PreDefinition.Structural.Eqns

source
structure Lean.Elab.Structural.EqnInfoextends Lean.Elab.Eqns.EqnInfoCore :
Type
  • recArgPos : Nat
source
instance Lean.Elab.Structural.instInhabitedEqnInfo:
Inhabited Lean.Elab.Structural.EqnInfo
Equations
source
def Lean.Elab.Structural.mkEqns (info : Lean.Elab.Structural.EqnInfo) :
Lean.MetaM (Array Lean.Name)
Equations
  • One or more equations did not get rendered due to their size.
source
opaque Lean.Elab.Structural.eqnInfoExt:
Lean.MapDeclarationExtension Lean.Elab.Structural.EqnInfo
source
def Lean.Elab.Structural.registerEqnsInfo (preDef : Lean.Elab.PreDefinition) (recArgPos : Nat) :
Lean.CoreM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Structural.getEqnsFor? (declName : Lean.Name) :
Lean.MetaM (Option (Array Lean.Name))
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Structural.getUnfoldFor? (declName : Lean.Name) :
Lean.MetaM (Option Lean.Name)
Equations
  • One or more equations did not get rendered due to their size.
source
@[export lean_get_structural_rec_arg_pos]
def Lean.Elab.Structural.getStructuralRecArgPosImp? (declName : Lean.Name) :
Lean.CoreM (Option Nat)
Equations
  • One or more equations did not get rendered due to their size.