Documentation

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

source
instance Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean :
Hashable Int.Linear.Expr
Equations
    source
    def Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean.hash :
    Int.Linear.Expr → UInt64
    Equations
      Instances For
        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
              Instances For

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

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