def Lean.Meta.Grind.Arith.Cutsat.mkNatVar (e : Expr) : GoalM Var

def Lean.Meta.Grind.Arith.Cutsat.getNatVars : GoalM (PArray Expr)

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

def Int.OfNat.toExpr (e : Expr) : Lean.Expr

instance Int.OfNat.instToExprExpr : Lean.ToExpr Expr

def Int.OfNat.Expr.denoteAsIntExpr (ctx : Lean.PArray Lean.Expr) (e : Expr) : Lean.Meta.Grind.GoalM Lean.Expr

def Int.OfNat.Expr.denoteAsIntExpr.go (ctx : Lean.PArray Lean.Expr) (e : Expr) : Lean.Expr

partial def Int.OfNat.toOfNatExpr (e : Lean.Expr) : Lean.Meta.Grind.GoalM Expr

def Int.OfNat.toIntLe? (e : Lean.Expr) : Lean.Meta.Grind.GoalM (Option (Expr × Expr))

Given e of the form lhs ≤ rhs where lhs and rhs have type Nat, returns (lhs, rhs) where lhs and rhs are Int.OfNat.Expr.

def Int.OfNat.toIntDvd? (e : Lean.Expr) : Lean.Meta.Grind.GoalM (Option (Nat × Expr))

def Int.OfNat.toIntEq (lhs rhs : Lean.Expr) : Lean.Meta.Grind.GoalM (Expr × Expr)

partial def Int.OfNat.ofDenoteAsIntExpr? (e : Lean.Expr) : OptionT Lean.Meta.Grind.GoalM Expr

Given e of type Int, tries to compute a : Int.OfNat.Expr s.t. a.denoteAsInt ctx is e

def Lean.Meta.Grind.Arith.Cutsat.assertDenoteAsIntNonneg (e : Expr) : GoalM Unit

If e is of the form a.denoteAsInt ctx for some a and ctx, assert that e is nonnegative.

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

Given x whose denotation is e, if e is of the form NatCast.natCast a, asserts that it is nonnegative.