Documentation

Lean.Meta.Constructions.CtorElim

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