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

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.getNatVars = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure __do_lift.natVars

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.natVarMap { expr := e })

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

Equations

• Int.OfNat.toExpr (Int.OfNat.Expr.num v) = Lean.mkApp (Lean.mkConst `Int.OfNat.Expr.num) (Lean.mkNatLit v)
• Int.OfNat.toExpr (Int.OfNat.Expr.var i) = Lean.mkApp (Lean.mkConst `Int.OfNat.Expr.var) (Lean.mkNatLit i)
• Int.OfNat.toExpr (a.add b) = Lean.mkApp2 (Lean.mkConst `Int.OfNat.Expr.add) (Int.OfNat.toExpr a) (Int.OfNat.toExpr b)
• Int.OfNat.toExpr (a.mul b) = Lean.mkApp2 (Lean.mkConst `Int.OfNat.Expr.mul) (Int.OfNat.toExpr a) (Int.OfNat.toExpr b)
• Int.OfNat.toExpr (a.div b) = Lean.mkApp2 (Lean.mkConst `Int.OfNat.Expr.div) (Int.OfNat.toExpr a) (Int.OfNat.toExpr b)
• Int.OfNat.toExpr (a.mod b) = Lean.mkApp2 (Lean.mkConst `Int.OfNat.Expr.mod) (Int.OfNat.toExpr a) (Int.OfNat.toExpr b)
• Int.OfNat.toExpr (a.pow k) = Lean.mkApp2 (Lean.mkConst `Int.OfNat.Expr.pow) (Int.OfNat.toExpr a) (Lean.mkNatLit k)

instance Int.OfNat.instToExprExpr : Lean.ToExpr Expr

Equations

• Int.OfNat.instToExprExpr = { toExpr := fun (a : Int.OfNat.Expr) => Int.OfNat.toExpr a, toTypeExpr := Lean.mkConst `Int.OfNat.Expr }

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

Equations

• Int.OfNat.Expr.denoteAsIntExpr ctx e = liftM (Lean.Meta.Grind.shareCommon (Int.OfNat.Expr.denoteAsIntExpr.go ctx e))

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

Equations

• Int.OfNat.Expr.denoteAsIntExpr.go ctx (Int.OfNat.Expr.num v) = Lean.mkIntLit ↑v
• Int.OfNat.Expr.denoteAsIntExpr.go ctx (Int.OfNat.Expr.var i) = Lean.mkIntNatCast ctx[i]!
• Int.OfNat.Expr.denoteAsIntExpr.go ctx (a.add b) = Lean.mkIntAdd (Int.OfNat.Expr.denoteAsIntExpr.go ctx a) (Int.OfNat.Expr.denoteAsIntExpr.go ctx b)
• Int.OfNat.Expr.denoteAsIntExpr.go ctx (a.mul b) = Lean.mkIntMul (Int.OfNat.Expr.denoteAsIntExpr.go ctx a) (Int.OfNat.Expr.denoteAsIntExpr.go ctx b)
• Int.OfNat.Expr.denoteAsIntExpr.go ctx (a.div b) = Lean.mkIntDiv (Int.OfNat.Expr.denoteAsIntExpr.go ctx a) (Int.OfNat.Expr.denoteAsIntExpr.go ctx b)
• Int.OfNat.Expr.denoteAsIntExpr.go ctx (a.mod b) = Lean.mkIntMod (Int.OfNat.Expr.denoteAsIntExpr.go ctx a) (Int.OfNat.Expr.denoteAsIntExpr.go ctx b)
• Int.OfNat.Expr.denoteAsIntExpr.go ctx (a.pow k) = Lean.mkIntPowNat (Int.OfNat.Expr.denoteAsIntExpr.go ctx a) (Lean.mkNatLit k)

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.

Equations

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

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

Equations

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

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

Equations

• Int.OfNat.toIntEq lhs rhs = do let lhs ← Int.OfNat.toOfNatExpr lhs let rhs ← Int.OfNat.toOfNatExpr rhs pure (lhs, rhs)

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.

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.