Documentation

Lean.Meta.Constructions.BRecOn

source
def Lean.mkBelow (indName : Name) :
MetaM Unit
Equations
    Instances For
      source
      def Lean.mkBRecOn (indName : Name) :
      MetaM Unit
      Equations
        Instances For