Documentation

Lean.Meta.Constructions.CtorElim

source
def Lean.mkCtorElimName (indName : Name) :
Name
Equations
    Instances For
      source
      def Lean.mkConstructorElimName (indName conName : Name) :
      Name
      Equations
        Instances For
          source
          def Lean.mkCtorElim (indName : Name) :
          MetaM Unit
          Equations
            Instances For