Documentation

Lean.Meta.Tactic.Grind.Order.Util

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