structure Lean.Meta.Grind.Order.OrderM.Context : Type

• structId : Nat

@[reducible, inline]

abbrev Lean.Meta.Grind.Order.OrderM (α : Type) : Type

Equations

• Lean.Meta.Grind.Order.OrderM = ReaderT Lean.Meta.Grind.Order.OrderM.Context Lean.Meta.Grind.GoalM

@[reducible, inline]

abbrev Lean.Meta.Grind.Order.OrderM.run {α : Type} (structId : Nat) (x : OrderM α) : GoalM α

Equations

• Lean.Meta.Grind.Order.OrderM.run structId x = x { structId := structId }

@[reducible, inline]

abbrev Lean.Meta.Grind.Order.getStructId : OrderM Nat

Equations

• Lean.Meta.Grind.Order.getStructId = do let __do_lift ← read pure __do_lift.structId

def Lean.Meta.Grind.Order.getOrder : OrderM Sym.Arith.Order

The Sym.Arith classification record (instances, ≤/< functions) of the current order.

Equations

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

def Lean.Meta.Grind.Order.getStruct : OrderM Struct

The per-goal solver state of the current order; empty if this goal has not used it yet.

Equations

• Lean.Meta.Grind.Order.getStruct = do let structId ← Lean.Meta.Grind.Order.getStructId let __do_lift ← liftM Lean.Meta.Grind.Order.get' pure (__do_lift.structs.getD structId { id := structId })

def Lean.Meta.Grind.Order.modifyStruct (f : Struct → Struct) : OrderM Unit

Equations

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

def Lean.Meta.Grind.Order.getExpr (u : NodeId) : OrderM Expr

Equations

• Lean.Meta.Grind.Order.getExpr u = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure __do_lift.nodes[u]!

def Lean.Meta.Grind.Order.getDist? (u v : NodeId) : OrderM (Option Weight)

Equations

• Lean.Meta.Grind.Order.getDist? u v = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure (Lean.AssocList.find? v __do_lift.targets[u]!)

def Lean.Meta.Grind.Order.getProof? (u v : NodeId) : OrderM (Option ProofInfo)

Equations

• Lean.Meta.Grind.Order.getProof? u v = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure (Lean.AssocList.find? v __do_lift.proofs[u]!)

def Lean.Meta.Grind.Order.getNodeId (e : Expr) : OrderM NodeId

Equations

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

def Lean.Meta.Grind.Order.getProof (u v : NodeId) : OrderM ProofInfo

Equations

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

def Lean.Meta.Grind.Order.getCnstr? (e : Expr) : OrderM (Option (Cnstr NodeId))

Equations

• Lean.Meta.Grind.Order.getCnstr? e = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure (Lean.PersistentHashMap.find? __do_lift.cnstrs { expr := e })

def Lean.Meta.Grind.Order.isRing : OrderM Bool

Equations

• Lean.Meta.Grind.Order.isRing = do let __do_lift ← Lean.Meta.Grind.Order.getOrder pure __do_lift.ringId?.isSome

def Lean.Meta.Grind.Order.isPartialOrder : OrderM Bool

Equations

• Lean.Meta.Grind.Order.isPartialOrder = do let __do_lift ← Lean.Meta.Grind.Order.getOrder pure __do_lift.isPartialInst?.isSome

def Lean.Meta.Grind.Order.isLinearPreorder : OrderM Bool

Equations

• Lean.Meta.Grind.Order.isLinearPreorder = do let __do_lift ← Lean.Meta.Grind.Order.getOrder pure __do_lift.isLinearPreInst?.isSome

def Lean.Meta.Grind.Order.hasLt : OrderM Bool

Equations

• Lean.Meta.Grind.Order.hasLt = do let __do_lift ← Lean.Meta.Grind.Order.getOrder pure __do_lift.lawfulOrderLTInst?.isSome

def Lean.Meta.Grind.Order.isInt : OrderM Bool

Equations

• Lean.Meta.Grind.Order.isInt = do let __do_lift ← Lean.Meta.Grind.Order.getOrder let __do_lift_1 ← liftM Lean.Meta.Sym.getIntExpr pure (Lean.Meta.Sym.isSameExpr __do_lift.type __do_lift_1)