def Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.isZero (b : SymbolicBound) : Bool

def Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.mkIntNegSucc (b : SymbolicBound) : MetaM Expr

Given a symbolic bound b, returns -b + 1

def Lean.Meta.Grind.Arith.Cutsat.getToIntId? (type : Expr) : GoalM (Option Nat)

structure Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context : Type

• toIntId : Nat

@[reducible, inline]

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

def Lean.Meta.Grind.Arith.Cutsat.getToIntId : ToIntM Nat

def Lean.Meta.Grind.Arith.Cutsat.getInfo : ToIntM ToIntInfo

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.modifyInfo (f : ToIntInfo → ToIntInfo) : ToIntM Unit

def Lean.Meta.Grind.Arith.Cutsat.ToIntM.run? {α : Type} (type : Expr) (x : ToIntM α) : GoalM (Option α)

def Lean.Meta.Grind.Arith.Cutsat.ToIntM.run (type : Expr) (x : ToIntM Unit) : GoalM Unit

def Lean.Meta.Grind.Arith.Cutsat.getOfLE? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getOfNotLE? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getOfLT? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getOfNotLT? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getAddThms : ToIntM ToIntThms

def Lean.Meta.Grind.Arith.Cutsat.getMulThms : ToIntM ToIntThms

def Lean.Meta.Grind.Arith.Cutsat.getSubThm? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getNegThm? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getDivThm? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getModThm? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getPowThm? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getZeroThm? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.getOfNatThm? : ToIntM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.mkToIntVar (e : Expr) : ToIntM (Expr × Expr)

def Lean.Meta.Grind.Arith.Cutsat.getToIntTermType? (e : Expr) : GoalM (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.isToIntTerm (e : Expr) : GoalM Bool

def Lean.Meta.Grind.Arith.Cutsat.toInt (a : Expr) : ToIntM (Expr × Expr)

def Lean.Meta.Grind.Arith.Cutsat.toInt? (a type : Expr) : GoalM (Option (Expr × Expr))

def Lean.Meta.Grind.Arith.Cutsat.isSupportedType (type : Expr) : GoalM Bool

def Lean.Meta.Grind.Arith.Cutsat.assertToIntBounds (e : Expr) (x : Var) : GoalM Unit

Given x whose denotation is e, if e is of the form ToInt a, asserts its lower and upper bounds if available