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

Given `e`, returns `(NatCast.natCast e, rfl)`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.natToInt (a : Expr) :
GoalM (Expr × Expr)

Given `a : Nat`, returns `(a', h)` such that `a' : Int`, and `h : NatCast.natCast a = a'`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- Lean.Meta.Grind.Arith.Cutsat.isNatTerm e = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure (Lean.PersistentHashMap.contains __do_lift.natToIntMap { expr := e })

Instances For

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

Given `e : Int`, tries to construct a proof that `e ≥ 0`

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Given `x` whose denotation is `e : Int`, tries to assert that `e ≥ 0`

Equations

- One or more equations did not get rendered due to their size.

Instances For