def Lean.Meta.Grind.Order.propagateEqTrue (c : Cnstr NodeId) (e : Expr) (u v : NodeId) (k k' : Weight) : OrderM Unit

def Lean.Meta.Grind.Order.propagateSelfEqTrue (c : Cnstr NodeId) (e : Expr) : OrderM Unit

def Lean.Meta.Grind.Order.propagateEqFalse (c : Cnstr NodeId) (e : Expr) (u v : NodeId) (k k' : Weight) : OrderM Unit

def Lean.Meta.Grind.Order.propagateSelfEqFalse (c : Cnstr NodeId) (e : Expr) : OrderM Unit

def Lean.Meta.Grind.Order.addEdge (u v : NodeId) (k : Weight) (h : Expr) : OrderM Unit

Adds an edge u --(k) --> v justified by the proof term p, and then if no negative cycle was created, updates the shortest distance of affected node pairs.

def Lean.Meta.Grind.Order.processNewEq (a b : Expr) : GoalM Unit