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

• structId : Nat

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

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

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

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

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

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

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

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

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

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

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

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

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

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