Documentation

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

source
def Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean.hash :
Int.Linear.Expr → UInt64
Instances For
    source
    @[implicit_reducible]
    instance Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean :
    Hashable Int.Linear.Expr
    source
    def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.toExprProof (h : UnsatProof) :
    GoalM Expr
    Instances For
      source
      def Lean.Meta.Grind.Arith.Cutsat.setInconsistent (h : UnsatProof) :
      GoalM Unit
      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
        Instances For