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 Lean.Name)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      opaque Lean.Elab.Structural.eqnInfoExt :
      Lean.MapDeclarationExtension Lean.Elab.Structural.EqnInfo
      source
      def Lean.Elab.Structural.registerEqnsInfo (preDef : Lean.Elab.PreDefinition) (declNames : Array Lean.Name) (recArgPos numFixed : Nat) :
      Lean.CoreM Unit
      Instances For
        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.
        Instances For
          source
          def Lean.Elab.Structural.getUnfoldFor? (declName : Lean.Name) :
          Lean.MetaM (Option Lean.Name)
          Instances For
            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.
            Instances For