source
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)

Instances For

source
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.

Instances For

source
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!)

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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₂)

Instances For