def Lean.Meta.Grind.Arith.Linear.toContextExpr (vars : Array Expr) : LinearM Expr

Returns a context of type RArray α containing the variables of the given structure, where α is (← getStruct).type.

Equations

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

structure Lean.Meta.Grind.Arith.Linear.ProofM.State : Type

• cache : Std.HashMap UInt64 Expr
• varDecls : Std.HashMap Var Expr
• polyDecls : Std.HashMap Poly Expr
• exprDecls : Std.HashMap LinExpr Expr
• ringPolyDecls : Std.HashMap CommRing.Poly Expr
• ringExprDecls : Std.HashMap CommRing.RingExpr Expr

structure Lean.Meta.Grind.Arith.Linear.ProofM.Context : Type

• ctx : Expr
• ringCtx : Expr

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.ProofM (α : Type) : Type

Auxiliary monad for constructing linarith proofs.

Equations

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

def Lean.Meta.Grind.Arith.Linear.mkVarDecl (x : Var) : ProofM Expr

Equations

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

def Lean.Meta.Grind.Arith.Linear.mkPolyDecl (p : Poly) : ProofM Expr

Equations

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

def Lean.Meta.Grind.Arith.Linear.mkExprDecl (e : LinExpr) : ProofM Expr

Equations

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

def Lean.Meta.Grind.Arith.Linear.mkRingPolyDecl (p : CommRing.Poly) : ProofM Expr

Equations

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

def Lean.Meta.Grind.Arith.Linear.mkRingExprDecl (e : CommRing.RingExpr) : ProofM Expr

Equations

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

partial def Lean.Meta.Grind.Arith.Linear.IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Linear.EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Linear.UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr

def Lean.Meta.Grind.Arith.Linear.UnsatProof.toExprProof (h : UnsatProof) : LinearM Expr

Equations

• h.toExprProof = Lean.Meta.Grind.Arith.Linear.withProofContext✝ h.toExprProofCore

def Lean.Meta.Grind.Arith.Linear.setInconsistent (h : UnsatProof) : LinearM Unit

Equations

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

A linarith proof may depend on decision variables. We collect them and perform non chronological backtracking.

partial def Lean.Meta.Grind.Arith.Linear.IneqCnstr.collectDecVars (c' : IneqCnstr) : CollectDecVarsM Unit

partial def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit

partial def Lean.Meta.Grind.Arith.Linear.EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit

def Lean.Meta.Grind.Arith.Linear.UnsatProof.collectDecVars (h : UnsatProof) : CollectDecVarsM Unit

Equations

• (Lean.Meta.Grind.Arith.Linear.UnsatProof.lt c).collectDecVars = c.collectDecVars
• (Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq c).collectDecVars = c.collectDecVars