def Lean.Meta.Grind.Order.mkLePreorderPrefix (declName : Name) : OrderM Expr

Returns declName α leInst isPreorderInst

def Lean.Meta.Grind.Order.mkLeLtLinearPrefix (declName : Name) : OrderM Expr

Returns declName α leInst ltInst lawfulOrderLtInst isLinearPreorderInst

def Lean.Meta.Grind.Order.mkLeLinearPrefix (declName : Name) : OrderM Expr

Returns declName α leInst isLinearPreorderInst

def Lean.Meta.Grind.Order.mkOrdRingPrefix (declName : Name) : OrderM Expr

Returns declName α leInst ltInst lawfulOrderLtInst isPreorderInst ringInst ordRingInst

def Lean.Meta.Grind.Order.mkLinearOrdRingPrefix (declName : Name) : OrderM Expr

Returns declName α leInst ltInst lawfulOrderLtInst isLinearPreorderInst ringInst ordRingInst

def Lean.Meta.Grind.Order.mkTrans (p₁ p₂ : ProofInfo) (v : NodeId) : OrderM ProofInfo

Assume p₁ is { w := u, k := k₁, proof := p₁ } and p₂ is { w := w, k := k₂, proof := p₂ } p₁ is the proof for edge u -(k₁)→ w and p₂ the proof for edge w -(k₂)-> v. Then, this function returns a proof for edge u -(k₁+k₂) -> v.

Remark: if the order does not support offset k₁ and k₂ are zero.

def Lean.Meta.Grind.Order.mkPropagateEqTrueProof (u v : Expr) (k : Weight) (huv : Expr) (k' : Weight) : OrderM Expr

Given a path u --(k)--> v justified by proof huv, construct a proof of e = True where e is a term corresponding to the edge u --(k') --> v

def Lean.Meta.Grind.Order.mkPropagateSelfEqTrueProof (u : Expr) (k : Weight) : OrderM Expr

Constructs a proof of e = True where e is a term corresponding to the edge u --(k) --> u with k non-negative

def Lean.Meta.Grind.Order.mkPropagateEqFalseProof (u v : Expr) (k : Weight) (huv : Expr) (k' : Weight) : OrderM Expr

Given a path u --(k)--> v justified by proof huv, construct a proof of e = False where e is a term corresponding to the edge u --(k') --> v

def Lean.Meta.Grind.Order.mkPropagateSelfEqFalseProof (u : Expr) (k : Weight) : OrderM Expr

Constructs a proof of e = False where e is a term corresponding to the edge u --(k) --> u and k is negative.

def Lean.Meta.Grind.Order.mkSelfUnsatProof (u : Expr) (k : Weight) (h : Expr) : OrderM Expr

Returns a proof of False using u --(k)--> u with proof h where k is negative

def Lean.Meta.Grind.Order.mkUnsatProof (u v : Expr) (k₁ : Weight) (h₁ : Expr) (k₂ : Weight) (h₂ : Expr) : OrderM Expr

Returns a proof of False using a negative cycle composed of

• u --(k₁)--> v with proof h₁
• v --(k₂)--> u with proof h₂

def Lean.Meta.Grind.Order.mkEqProofOfLeOfLeCore (u v h₁ h₂ : Expr) : OrderM Expr

def Lean.Meta.Grind.Order.mkEqProofOfLeOfLeOffset (u v h₁ h₂ : Expr) : OrderM Expr

def Lean.Meta.Grind.Order.mkEqProofOfLeOfLe (u v h₁ h₂ : Expr) : OrderM Expr