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.

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
• ringVarDecls : Std.HashMap Var 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.

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

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

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

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

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

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

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

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

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

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

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

def Lean.Meta.Grind.Arith.Linear.propagateImpEq (c : EqCnstr) : LinearM Unit

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