def Lean.Meta.Grind.Order.Cnstr.pp (c : Cnstr NodeId) : OrderM MessageData

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Order.Weight.compare (a b : Weight) : Ordering

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Meta.Grind.Order.instOrdWeight : Ord Weight

Equations

• Lean.Meta.Grind.Order.instOrdWeight = { compare := Lean.Meta.Grind.Order.Weight.compare }

@[implicit_reducible]

instance Lean.Meta.Grind.Order.instLEWeight : LE Weight

Equations

• Lean.Meta.Grind.Order.instLEWeight = { le := fun (a b : Lean.Meta.Grind.Order.Weight) => compare a b ≠ Ordering.gt }

@[implicit_reducible]

instance Lean.Meta.Grind.Order.instLTWeight : LT Weight

Equations

• Lean.Meta.Grind.Order.instLTWeight = { lt := fun (a b : Lean.Meta.Grind.Order.Weight) => compare a b = Ordering.lt }

@[implicit_reducible]

instance Lean.Meta.Grind.Order.instDecidableLEWeight : DecidableLE Weight

Equations

• Lean.Meta.Grind.Order.instDecidableLEWeight a b = match instDecidableEqOrdering (compare a b) Ordering.gt with | isTrue hp => isFalse ⋯ | isFalse hp => isTrue hp

@[implicit_reducible]

instance Lean.Meta.Grind.Order.instDecidableLTWeight : DecidableLT Weight

Equations

• Lean.Meta.Grind.Order.instDecidableLTWeight a b = if h : (compare a b).ctorIdx = Ordering.lt.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lean.Meta.Grind.Order.Weight.add (a b : Weight) : Weight

Equations

• a.add b = { k := a.k + b.k, strict := a.strict || b.strict }

@[implicit_reducible]

instance Lean.Meta.Grind.Order.instAddWeight : Add Weight

Equations

• Lean.Meta.Grind.Order.instAddWeight = { add := Lean.Meta.Grind.Order.Weight.add }

def Lean.Meta.Grind.Order.Weight.isNeg (a : Weight) : Bool

Equations

• a.isNeg = (decide (a.k < 0) || a.k == 0 && a.strict)

def Lean.Meta.Grind.Order.Weight.isZero (a : Weight) : Bool

Equations

• a.isZero = (a.k == 0 && !a.strict)

@[implicit_reducible]

instance Lean.Meta.Grind.Order.instToStringWeight : ToString Weight

Equations

• Lean.Meta.Grind.Order.instToStringWeight = { toString := fun (a : Lean.Meta.Grind.Order.Weight) => if a.strict = true then toString a.k ++ toString "-ε" else toString a.k }

def Lean.Meta.Grind.Order.ToPropagate.pp (todo : ToPropagate) : OrderM MessageData

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Order.Cnstr.getWeight {α : Type} (c : Cnstr α) : Weight

Equations

• c.getWeight = match c.kind with | Lean.Meta.Grind.Order.CnstrKind.le => { k := c.k } | Lean.Meta.Grind.Order.CnstrKind.lt => { k := c.k, strict := true }