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

Returns declName α leInst isPreorderInst

Equations

• Lean.Meta.Grind.Order.mkLePreorderPrefix declName = do let s ← Lean.Meta.Grind.Order.getStruct pure (Lean.mkApp3 (Lean.mkConst declName [s.u]) s.type s.leInst s.isPreorderInst)

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

Returns declName α leInst ltInst lawfulOrderLtInst isLinearPreorderInst

Equations

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

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

Returns declName α leInst isLinearPreorderInst

Equations

• Lean.Meta.Grind.Order.mkLeLinearPrefix declName = do let s ← Lean.Meta.Grind.Order.getStruct pure (Lean.mkApp3 (Lean.mkConst declName [s.u]) s.type s.leInst s.isLinearPreInst?.get!)

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

Returns declName α leInst ltInst lawfulOrderLtInst isPreorderInst ringInst ordRingInst

Equations

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

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

Returns declName α leInst ltInst lawfulOrderLtInst isLinearPreorderInst ringInst ordRingInst

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

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₂

Equations

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

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

Equations

• Lean.Meta.Grind.Order.mkEqProofOfLeOfLe u v h₁ h₂ = do let h ← Lean.Meta.Grind.Order.mkLePartialPrefix✝ `Lean.Grind.Order.eq_of_le_of_le pure (Lean.mkApp4 h u v h₁ h₂)