Documentation

Lean.Meta.Injective

source
def Lean.Meta.elimOptParam (type : Expr) :
CoreM Expr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.mkInjectiveTheoremNameFor (ctorName : Name) :
    Name
    Equations
    Instances For
      source
      def Lean.Meta.mkInjectiveEqTheoremNameFor (ctorName : Name) :
      Name
      Equations
      Instances For
        source
        opaque Lean.Meta.genInjectivity :
        Lean.Option Bool
        source
        def Lean.Meta.mkInjectiveTheorems (declName : Name) :
        MetaM Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For