Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof

source
partial def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.toExprProof (c' : EqCnstr) :
ProofM Expr
source
partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.toExprProof (c' : DvdCnstr) :
ProofM Expr
source
partial def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.toExprProof (c' : LeCnstr) :
ProofM Expr
source
partial def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.toExprProof (c' : DiseqCnstr) :
ProofM Expr
source
partial def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.toExprProofCore (h : UnsatProof) :
ProofM Expr
source
def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.toExprProof (h : UnsatProof) :
GoalM Expr
Equations
Instances For
    source
    def Lean.Meta.Grind.Arith.Cutsat.setInconsistent (h : UnsatProof) :
    GoalM Unit
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      source
      structure Lean.Meta.Grind.Arith.Cutsat.CollectDecVars.State :
      Type
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Meta.Grind.Arith.Cutsat.CollectDecVarsM (α : Type) :
        Type
        Equations
        Instances For
          source
          partial def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.collectDecVars (c' : EqCnstr) :
          CollectDecVarsM Unit
          source
          partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.collectDecVars (c' : DvdCnstr) :
          CollectDecVarsM Unit
          source
          partial def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.collectDecVars (c' : LeCnstr) :
          CollectDecVarsM Unit
          source
          partial def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.collectDecVars (c' : DiseqCnstr) :
          CollectDecVarsM Unit
          source
          def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.collectDecVars (h : UnsatProof) :
          CollectDecVarsM Unit
          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Lean.Meta.Grind.Arith.Cutsat.CollectDecVarsM.run (x : CollectDecVarsM Unit) (decVars : FVarIdSet) :
            FVarIdSet
            Equations
            Instances For