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
      • 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
        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