Documentation

Lean.Meta.Constructions.BRecOn

source
def Lean.mkBelow (declName : Lean.Name) :
Lean.MetaM Unit
Equations
Instances For
    source
    def Lean.mkIBelow (declName : Lean.Name) :
    Lean.MetaM Unit
    Instances For
      source
      def Lean.mkBRecOnOrBInductionOn (indName : Lean.Name) (ind : Bool) :
      Lean.MetaM Unit
      Instances For
        source
        def Lean.mkBRecOn (declName : Lean.Name) :
        Lean.MetaM Unit
        Instances For
          source
          def Lean.mkBInductionOn (declName : Lean.Name) :
          Lean.MetaM Unit
          Equations
          Instances For