Documentation

Lean.Meta.Injective

source
def Lean.Meta.elimOptParam (type : Lean.Expr) :
Lean.CoreM Lean.Expr
Instances For
    source
    def Lean.Meta.mkInjectiveTheoremNameFor (ctorName : Lake.Name) :
    Lake.Name
    Instances For
      source
      def Lean.Meta.mkInjectiveEqTheoremNameFor (ctorName : Lake.Name) :
      Lake.Name
      Instances For
        source
        opaque Lean.Meta.genInjectivity :
        Lean.Option Bool
        source
        def Lean.Meta.mkInjectiveTheorems (declName : Lake.Name) :
        Lean.MetaM Unit
        Instances For