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

Instances For

source
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

Instances For

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

- ctx : Expr
- ringCtx : Expr

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

source
partial def Lean.Meta.Grind.Arith.Linear.IneqCnstr.toExprProof (c' : IneqCnstr) :
ProofM Expr
source
partial def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.toExprProof (c' : DiseqCnstr) :
ProofM Expr
source
partial def Lean.Meta.Grind.Arith.Linear.EqCnstr.toExprProof (c' : EqCnstr) :
ProofM Expr
source
partial def Lean.Meta.Grind.Arith.Linear.UnsatProof.toExprProofCore (h : UnsatProof) :
ProofM Expr
source
def Lean.Meta.Grind.Arith.Linear.UnsatProof.toExprProof (h : UnsatProof) :
LinearM Expr
Equations

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

Instances For

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

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

Instances For

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

source
partial def Lean.Meta.Grind.Arith.Linear.IneqCnstr.collectDecVars (c' : IneqCnstr) :
CollectDecVarsM Unit
source
partial def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.collectDecVars (c' : DiseqCnstr) :
CollectDecVarsM Unit
source
partial def Lean.Meta.Grind.Arith.Linear.EqCnstr.collectDecVars (c' : EqCnstr) :
CollectDecVarsM Unit
source
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

Instances For