Documentation

Lean.Meta.Tactic.Grind.OrderInsts

Helper function for synthesizing order related instances.

source
def Lean.Meta.Grind.mkLawfulOrderLTInst? (u : Level) (type : Expr) (ltInst? leInst? : Option Expr) :
GoalM (Option Expr)
Instances For
    source
    def Lean.Meta.Grind.mkIsPreorderInst? (u : Level) (type : Expr) (leInst? : Option Expr) :
    GoalM (Option Expr)
    Instances For
      source
      def Lean.Meta.Grind.mkIsPartialOrderInst? (u : Level) (type : Expr) (leInst? : Option Expr) :
      GoalM (Option Expr)
      Instances For
        source
        def Lean.Meta.Grind.mkIsLinearOrderInst? (u : Level) (type : Expr) (leInst? : Option Expr) :
        GoalM (Option Expr)
        Instances For
          source
          def Lean.Meta.Grind.mkIsLinearPreorderInst? (u : Level) (type : Expr) (leInst? : Option Expr) :
          GoalM (Option Expr)
          Instances For