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)

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 : Array Lean.Expr) (e : Expr) : Lean.Expr

Equations

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

structure Int.OfNat.OfNat.State : Type

• ctx : Array Lean.Expr
• map : Std.HashMap Lean.Meta.Grind.ENodeKey Var

@[reducible, inline]

abbrev Int.OfNat.M (α : Type) : Type

Equations

• Int.OfNat.M = StateRefT' IO.RealWorld Int.OfNat.OfNat.State Lean.MetaM

partial def Int.OfNat.toOfNatExpr (e : Lean.Expr) : M Expr

def Int.OfNat.toIntLe? (e : Lean.Expr) : Lean.MetaM (Option (Expr × Expr × Array Lean.Expr))

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

Equations

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

def Int.OfNat.toIntLe?.conv (lhs rhs : Lean.Expr) : M (Expr × Expr)

Equations

• Int.OfNat.toIntLe?.conv lhs rhs = do let __do_lift ← Int.OfNat.toOfNatExpr lhs let __do_lift_1 ← Int.OfNat.toOfNatExpr rhs pure (__do_lift, __do_lift_1)

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

Equations

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

def Int.OfNat.toIntEq (lhs rhs : Lean.Expr) : Lean.MetaM (Expr × Expr × Array Lean.Expr)

Equations

• Int.OfNat.toIntEq lhs rhs = do let __discr ← StateRefT'.run (Int.OfNat.toIntEq.conv lhs rhs) { } match __discr with | ((lhs, rhs), s) => pure (lhs, rhs, s.ctx)

def Int.OfNat.toIntEq.conv (lhs rhs : Lean.Expr) : M (Expr × Expr)

Equations

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

partial def Int.OfNat.ofDenoteAsIntExpr? (e : Lean.Expr) : OptionT M 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.