This file defines a signed 64-bit integer datatype similar to Rust's i64 by adding checked arithmetic operations to Lean's Int64 datatype.

def Int64.MIN : Int

Equations

• Int64.MIN = -9223372036854775808

def Int64.MAX : Int

Equations

• Int64.MAX = 9223372036854775807

def Int64.ofIntChecked (i : Int) : MIN ≤ i ∧ i ≤ MAX → Int64

Equations

• Int64.ofIntChecked i x✝ = Int64.ofInt i

def Int64.ofInt? (i : Int) : Option Int64

Equations

• Int64.ofInt? i = if h : Int64.MIN ≤ i ∧ i ≤ Int64.MAX then some (Int64.ofIntChecked i h) else none

theorem Int64.ofInt?_some_iff {i : Int} : MIN ≤ i ∧ i ≤ MAX ↔ ofInt? i = some (ofInt i)

We don't @[expose] the definition of ofInt?; but callers can use this theorem, which specifies its behavior

theorem Int64.ofInt?_none_iff {i : Int} : i < MIN ∨ i > MAX ↔ ofInt? i = none

Inverse of the above

def Int64.add? (i₁ i₂ : Int64) : Option Int64

Equations

• i₁.add? i₂ = Int64.ofInt? (i₁.toInt + i₂.toInt)

def Int64.sub? (i₁ i₂ : Int64) : Option Int64

Equations

• i₁.sub? i₂ = Int64.ofInt? (i₁.toInt - i₂.toInt)

def Int64.mul? (i₁ i₂ : Int64) : Option Int64

Equations

• i₁.mul? i₂ = Int64.ofInt? (i₁.toInt * i₂.toInt)

def Int64.neg? (i₁ : Int64) : Option Int64

Equations

• i₁.neg? = Int64.ofInt? (-i₁.toInt)

def Int64.natAbs (i₁ : Int64) : Nat

Equations

• i₁.natAbs = i₁.toInt.natAbs

instance Int64.instRepr_cedar : Repr Int64

Equations

• Int64.instRepr_cedar = { reprPrec := Int64.instRepr_cedar.repr }

def Int64.instRepr_cedar.repr : Int64 → Nat → Std.Format

Equations

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

instance Int64.strictLT : Cedar.Data.StrictLT Int64

instance Int64.instCoeInt_cedar : Coe Int64 Int

Equations

• Int64.instCoeInt_cedar = { coe := fun (i : Int64) => i.toInt }