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

def Int64.smod (a b : Int64) : Int64

A version of Int64.mod with the property that b > 0 → ∀ a, 0 <= smod a b < b

Equations

• a.smod b = Int64.ofBitVec (a.toBitVec.smod b.toBitVec)

theorem Int64.smod_result_nonneg {a b : Int64} : b > 0 → 0 ≤ a.smod b ∧ a.smod b < b

theorem Int64.toInt_smod (a b : Int64) : (a.smod b).toInt = a.toInt.fmod b.toInt

theorem Int64.ofInt?_toInt (v : Int64) : ofInt? v.toInt = some v

theorem Int64.ofInt?_some_toInt {n : Int} {i : Int64} (h : ofInt? n = some i) : i.toInt = n

ofInt? roundtrip: when it succeeds, coercing the result back to Int recovers the original value. This is the converse companion to ofInt?_toInt.

theorem Int64.toInt_nonneg_of_ge_zero {v : Int64} (h : v ≥ 0) : v.toInt ≥ 0

theorem Int64.toInt_neg_of_not_ge_zero {v : Int64} (h : ¬v ≥ 0) : v.toInt < 0

theorem Int64.lt_def_toInt {i₁ i₂ : Int64} : i₁ < i₂ ↔ i₁.toInt < i₂.toInt

theorem Int64.le_def_toInt {i₁ i₂ : Int64} : i₁ ≤ i₂ ↔ i₁.toInt ≤ i₂.toInt

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

Equations

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

@[instance_reducible]

instance Int64.instRepr_cedar : Repr Int64

Equations

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

instance Int64.strictLT : Cedar.Data.StrictLT Int64

@[instance_reducible]

instance Int64.instCoeInt_cedar : Coe Int64 Int

Equations

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