source
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.

Instances For

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

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

Instances For

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

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

source
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 }

source
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 }

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

- Lean.Meta.Grind.Order.instDecidableLEWeight a b = inferInstanceAs (Decidable (compare a b ≠ Ordering.gt))

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

- Lean.Meta.Grind.Order.instDecidableLTWeight a b = inferInstanceAs (Decidable (compare a b = Ordering.lt))

source
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 }

Instances For

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

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

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

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

Instances For

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

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

Instances For

source
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 }

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

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

Instances For

source
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 }

Instances For