Documentation

Lean.Meta.Injective

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