Documentation

Lean.Meta.Injective

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