Documentation

Lean.Meta.Tactic.Grind.Order.Util

source
def Lean.Meta.Grind.Order.Cnstr.pp (c : Cnstr NodeId) :
OrderM MessageData
Instances For
    source
    def Lean.Meta.Grind.Order.Weight.compare (a b : Weight) :
    Ordering
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Meta.Grind.Order.instOrdWeight :
      Ord Weight
      source
      @[implicit_reducible]
      instance Lean.Meta.Grind.Order.instLEWeight :
      LE Weight
      source
      @[implicit_reducible]
      instance Lean.Meta.Grind.Order.instLTWeight :
      LT Weight
      source
      @[implicit_reducible]
      instance Lean.Meta.Grind.Order.instDecidableLEWeight :
      DecidableLE Weight
      source
      @[implicit_reducible]
      instance Lean.Meta.Grind.Order.instDecidableLTWeight :
      DecidableLT Weight
      source
      def Lean.Meta.Grind.Order.Weight.add (a b : Weight) :
      Weight
      Instances For
        source
        @[implicit_reducible]
        instance Lean.Meta.Grind.Order.instAddWeight :
        Add Weight
        source
        def Lean.Meta.Grind.Order.Weight.isNeg (a : Weight) :
        Bool
        Instances For
          source
          def Lean.Meta.Grind.Order.Weight.isZero (a : Weight) :
          Bool
          Instances For
            source
            @[implicit_reducible]
            instance Lean.Meta.Grind.Order.instToStringWeight :
            ToString Weight
            source
            def Lean.Meta.Grind.Order.ToPropagate.pp (todo : ToPropagate) :
            OrderM MessageData
            Instances For
              source
              def Lean.Meta.Grind.Order.Cnstr.getWeight {α : Type} (c : Cnstr α) :
              Weight
              Instances For