Documentation

Lean.Elab.PreDefinition.Structural.Eqns

source
structure Lean.Elab.Structural.EqnInfoextends Lean.Elab.Eqns.EqnInfoCore :
Type
Instances For
    source
    instance Lean.Elab.Structural.instInhabitedEqnInfo :
    Inhabited Lean.Elab.Structural.EqnInfo
    source
    def Lean.Elab.Structural.mkEqns (info : Lean.Elab.Structural.EqnInfo) :
    Lean.MetaM (Array Lake.Name)
    Instances For
      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
      Instances For
        source
        def Lean.Elab.Structural.getEqnsFor? (declName : Lake.Name) :
        Lean.MetaM (Option (Array Lake.Name))
        Instances For
          source
          def Lean.Elab.Structural.getUnfoldFor? (declName : Lake.Name) :
          Lean.MetaM (Option Lake.Name)
          Instances For
            source
            @[export lean_get_structural_rec_arg_pos]
            def Lean.Elab.Structural.getStructuralRecArgPosImp? (declName : Lake.Name) :
            Lean.CoreM (Option Nat)
            Instances For