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

Given e, returns (NatCast.natCast e, rfl). The new term ↑e is internalized before e is marked as a solver term: marking replays pending equalities of e into processNewEq, which reifies ↑e.

Equations

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

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.

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.

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 })

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.

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.