def Std.Time.Internal.Bounded (rel : Int → Int → Prop) (lo hi : Int) : Type

A Bounded is represented by an Int that is constrained by a lower and higher bounded using some relation rel. It includes all the integers that rel lo val ∧ rel val hi.

@[instance_reducible, always_inline]

instance Std.Time.Internal.Bounded.instLE {rel : Int → Int → Prop} {n m : Int} : _root_.LE (Bounded rel n m)

@[instance_reducible, always_inline]

instance Std.Time.Internal.Bounded.instLT {rel : Int → Int → Prop} {n m : Int} : _root_.LT (Bounded rel n m)

@[instance_reducible, always_inline]

instance Std.Time.Internal.Bounded.instOrd {rel : Int → Int → Prop} {n m : Int} : Ord (Bounded rel n m)

@[instance_reducible, always_inline]

instance Std.Time.Internal.Bounded.instRepr {rel : Int → Int → Prop} {m n : Int} : Repr (Bounded rel m n)

@[instance_reducible, always_inline]

instance Std.Time.Internal.Bounded.instDecidableEq {rel : Int → Int → Prop} {n m : Int} : DecidableEq (Bounded rel n m)

@[instance_reducible, always_inline]

instance Std.Time.Internal.Bounded.instDecidableLe {rel : Int → Int → Prop} {a b : Int} {x y : Bounded rel a b} : Decidable (x ≤ y)

instance Std.Time.Internal.Bounded.instOrientedOrd {rel : Int → Int → Prop} {n m : Int} : OrientedOrd (Bounded rel n m)

instance Std.Time.Internal.Bounded.instTransOrd {rel : Int → Int → Prop} {n m : Int} : TransOrd (Bounded rel n m)

instance Std.Time.Internal.Bounded.instLawfulEqOrd {rel : Int → Int → Prop} {n m : Int} : LawfulEqOrd (Bounded rel n m)

@[reducible, inline]

abbrev Std.Time.Internal.Bounded.LE (lo hi : Int) : Type

A Bounded integer where the relation used is the less-equal relation, so it includes all integers that lo ≤ val ≤ hi.

@[inline]

def Std.Time.Internal.Bounded.cast {rel : Int → Int → Prop} {lo₁ lo₂ hi₁ hi₂ : Int} (h₁ : lo₁ = lo₂) (h₂ : hi₁ = hi₂) (b : Bounded rel lo₁ hi₁) : Bounded rel lo₂ hi₂

Casts the boundaries of the Bounded using equivalences.

@[reducible, inline]

abbrev Std.Time.Internal.Bounded.LT (lo hi : Int) : Type

A Bounded integer where the relation used is the less-than relation, so it includes all integers that lo < val < hi.

@[inline]

def Std.Time.Internal.Bounded.mk {lo hi : Int} {rel : Int → Int → Prop} (val : Int) (proof : rel lo val ∧ rel val hi) : Bounded rel lo hi

Creates a new Bounded Integer.

@[inline]

def Std.Time.Internal.Bounded.ofInt? {rel : Int → Int → Prop} {lo hi : Int} [DecidableRel rel] (val : Int) : Option (Bounded rel lo hi)

Convert a Int to a Bounded if it checks.

@[inline]

def Std.Time.Internal.Bounded.LE.ofNatWrapping {lo hi : Int} (val : Int) (h : lo ≤ hi) : LE lo hi

Convert a Nat to a Bounded.LE by wrapping it.

@[instance_reducible]

instance Std.Time.Internal.Bounded.LE.instOfNatHAddIntCast {lo : Int} {n k : Nat} : OfNat (LE lo (lo + ↑k)) n

@[instance_reducible]

instance Std.Time.Internal.Bounded.LE.instInhabitedHAddIntCast {lo : Int} {k : Nat} : Inhabited (LE lo (lo + ↑k))

@[inline]

def Std.Time.Internal.Bounded.LE.mk {lo hi : Int} (val : Int) (proof : lo ≤ val ∧ val ≤ hi) : LE lo hi

Creates a new Bounded integer that the relation is less-equal.

@[inline]

def Std.Time.Internal.Bounded.LE.exact (val : Nat) : LE ↑val ↑val

Creates a new Bounded integer that the relation is less-equal.

@[inline]

def Std.Time.Internal.Bounded.LE.ofInt {lo hi : Int} (val : Int) : Option (LE lo hi)

Creates a new Bounded integer.

@[inline]

def Std.Time.Internal.Bounded.LE.ofNat {hi : Nat} (val : Nat) (h : val ≤ hi) : LE 0 ↑hi

Convert a Nat to a Bounded.LE.

@[inline]

def Std.Time.Internal.Bounded.LE.ofNat? {hi : Nat} (val : Nat) : Option (LE 0 ↑hi)

Convert a Nat to a Bounded.LE if it checks.

@[inline]

def Std.Time.Internal.Bounded.LE.ofNat' {lo hi : Nat} (val : Nat) (h : lo ≤ val ∧ val ≤ hi) : LE ↑lo ↑hi

Convert a Nat to a Bounded.LE using the lower boundary too.

@[inline]

def Std.Time.Internal.Bounded.LE.clip {lo hi : Int} (val : Int) (h : lo ≤ hi) : LE lo hi

Convert a Nat to a Bounded.LE using the lower boundary too.

@[inline]

def Std.Time.Internal.Bounded.LE.toNat {lo hi : Int} (n : LE lo hi) : Nat

Convert a Bounded.LE to a Nat.

@[inline]

def Std.Time.Internal.Bounded.LE.toNat' {lo hi : Int} (n : LE lo hi) (h : lo ≥ 0) : Nat

Convert a Bounded.LE to a Nat.

@[inline]

def Std.Time.Internal.Bounded.LE.toInt {lo hi : Int} (n : LE lo hi) : Int

Convert a Bounded.LE to an Int.

@[inline]

def Std.Time.Internal.Bounded.LE.toFin {lo hi : Int} (n : LE lo hi) (h₀ : 0 ≤ lo) : Fin (hi + 1).toNat

Convert a Bounded.LE to a Fin.

@[inline]

def Std.Time.Internal.Bounded.LE.ofFin {hi : Nat} (fin : Fin hi.succ) : LE 0 ↑hi

Convert a Fin to a Bounded.LE.

@[inline]

def Std.Time.Internal.Bounded.LE.ofFin' {hi lo : Nat} (fin : Fin hi.succ) (h : lo ≤ hi) : LE ↑lo ↑hi

Convert a Fin to a Bounded.LE.

@[inline]

def Std.Time.Internal.Bounded.LE.byEmod (b i : Int) (hi : i > 0) : LE 0 (i - 1)

Creates a new Bounded.LE using the modulus of a number.

@[inline]

def Std.Time.Internal.Bounded.LE.byMod (b i : Int) (hi : 0 < i) : LE (-(i - 1)) (i - 1)

Creates a new Bounded.LE using the Truncating modulus of a number.

@[inline]

def Std.Time.Internal.Bounded.LE.truncate {n m : Int} (bounded : LE n m) : LE 0 (m - n)

Adjust the bounds of a Bounded by setting the lower bound to zero and the maximum value to (m - n).

@[inline]

def Std.Time.Internal.Bounded.LE.truncateTop {n m j : Int} (bounded : LE n m) (h : bounded.val ≤ j) : LE n j

Adjust the bounds of a Bounded by changing the higher bound if another value j satisfies the same constraint.

@[inline]

def Std.Time.Internal.Bounded.LE.truncateBottom {n m j : Int} (bounded : LE n m) (h : bounded.val ≥ j) : LE j m

Adjust the bounds of a Bounded by changing the lower bound if another value j satisfies the same constraint.

@[inline]

def Std.Time.Internal.Bounded.LE.neg {n m : Int} (bounded : LE n m) : LE (-m) (-n)

Adjust the bounds of a Bounded by adding a constant value to both the lower and upper bounds.

@[inline]

def Std.Time.Internal.Bounded.LE.add {n m : Int} (bounded : LE n m) (num : Int) : LE (n + num) (m + num)

Adjust the bounds of a Bounded by adding a constant value to both the lower and upper bounds.

@[inline]

def Std.Time.Internal.Bounded.LE.addProven {n m num : Int} (bounded : LE n m) (h₀ : bounded.val + num ≤ m) (h₁ : num ≥ 0) : LE n m

Adjust the bounds of a Bounded by adding a constant value to both the lower and upper bounds.

@[inline]

def Std.Time.Internal.Bounded.LE.addTop {n m : Int} (bounded : LE n m) (num : Int) (h : num ≥ 0) : LE n (m + num)

Adjust the bounds of a Bounded by adding a constant value to the upper bounds.

@[inline]

def Std.Time.Internal.Bounded.LE.subBottom {n m : Int} (bounded : LE n m) (num : Int) (h : num ≥ 0) : LE (n - num) m

Adjust the bounds of a Bounded by adding a constant value to the lower bounds.

@[inline]

def Std.Time.Internal.Bounded.LE.addBounds {n m i j : Int} (bounded : LE n m) (bounded₂ : LE i j) : LE (n + i) (m + j)

Adds two Bounded and adjust the boundaries.

@[inline]

def Std.Time.Internal.Bounded.LE.sub {n m : Int} (bounded : LE n m) (num : Int) : LE (n - num) (m - num)

Adjust the bounds of a Bounded by subtracting a constant value to both the lower and upper bounds.

@[inline]

def Std.Time.Internal.Bounded.LE.subBounds {n m i j : Int} (bounded : LE n m) (bounded₂ : LE i j) : LE (n - j) (m - i)

Adds two Bounded and adjust the boundaries.

@[inline]

def Std.Time.Internal.Bounded.LE.emod {n num : Int} (bounded : LE n num) (num✝ : Int) (hi : 0 < num✝) : LE 0 (num✝ - 1)

Adjust the bounds of a Bounded by applying the emod operation constraining the lower bound to 0 and the upper bound to the value.

@[inline]

def Std.Time.Internal.Bounded.LE.mod {n num : Int} (bounded : LE n num) (num✝ : Int) (hi : 0 < num✝) : LE (-(num✝ - 1)) (num✝ - 1)

Adjust the bounds of a Bounded by applying the mod operation.

@[inline]

def Std.Time.Internal.Bounded.LE.mul_pos {n m : Int} (bounded : LE n m) (num : Int) (h : num ≥ 0) : LE (n * num) (m * num)

Adjust the bounds of a Bounded by applying the multiplication operation with a positive number.

@[inline]

def Std.Time.Internal.Bounded.LE.mul_neg {n m : Int} (bounded : LE n m) (num : Int) (h : num ≤ 0) : LE (m * num) (n * num)

Adjust the bounds of a Bounded by applying the multiplication operation with a positive number.

@[inline]

def Std.Time.Internal.Bounded.LE.ediv {n m : Int} (bounded : LE n m) (num : Int) (h : num > 0) : LE (n / num) (m / num)

Adjust the bounds of a Bounded by applying the div operation.

@[inline]

def Std.Time.Internal.Bounded.LE.eq {n : Int} : LE n n

@[inline]

def Std.Time.Internal.Bounded.LE.expand {lo hi nhi nlo : Int} (bounded : LE lo hi) (h : hi ≤ nhi) (h₁ : nlo ≤ lo) : LE nlo nhi

Expand the range of a bounded value.

@[inline]

def Std.Time.Internal.Bounded.LE.expandTop {lo hi nhi : Int} (bounded : LE lo hi) (h : hi ≤ nhi) : LE lo nhi

Expand the bottom of the bounded to a number nhi is hi is less or equal to the previous higher bound.

@[inline]

def Std.Time.Internal.Bounded.LE.expandBottom {lo hi nlo : Int} (bounded : LE lo hi) (h : nlo ≤ lo) : LE nlo hi

Expand the bottom of the bounded to a number nlo if lo is greater or equal to the previous lower bound.

@[inline]

def Std.Time.Internal.Bounded.LE.succ {lo hi : Int} (bounded : LE lo hi) (h : bounded.val < hi) : LE lo hi

Adds one to the value of the bounded if the value is less than the higher bound of the bounded number.

@[inline]

def Std.Time.Internal.Bounded.LE.abs {i : Int} (bo : LE (-i) i) : LE 0 i

Returns the absolute value of the bounded number bo with bounds -(i - 1) to i - 1. The result will be a new bounded number with bounds 0 to i - 1.

def Std.Time.Internal.Bounded.LE.max {n m : Int} (bounded : LE n m) (val : Int) : LE (Max.max n val) (Max.max m val)

Returns the maximum between a number and the bounded.