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

partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr

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

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

def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.toExprProof (h : UnsatProof) : GoalM Expr

Equations

• h.toExprProof = Lean.Meta.Grind.Arith.Cutsat.withProofContext h.toExprProofCore

def Lean.Meta.Grind.Arith.Cutsat.setInconsistent (h : UnsatProof) : GoalM Unit

Equations

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

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

structure Lean.Meta.Grind.Arith.Cutsat.CollectDecVars.State : Type

• visited : Std.HashSet Nat
• found : FVarIdSet

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.CollectDecVarsM (α : Type) : Type

Equations

• Lean.Meta.Grind.Arith.Cutsat.CollectDecVarsM = ReaderT Lean.FVarIdSet (StateM Lean.Meta.Grind.Arith.Cutsat.CollectDecVars.State)

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

partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit

partial def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit

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

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

Equations

• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le c).collectDecVars = c.collectDecVars
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd c).collectDecVars = c.collectDecVars
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq c).collectDecVars = c.collectDecVars
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq c).collectDecVars = c.collectDecVars

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.CollectDecVarsM.run (x : CollectDecVarsM Unit) (decVars : FVarIdSet) : FVarIdSet

Equations

• x.run decVars = match StateT.run (x decVars) { visited := ∅, found := ∅ } with | (fst, s) => s.found