source
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`.

Equations

- Std.Time.Internal.Bounded rel lo hi = { val : Int // rel lo val ∧ rel val hi }

Instances For

source
@[always_inline]
instance Std.Time.Internal.Bounded.instLE {rel : Int → Int → Prop} {n m : Int} :
_root_.LE (Bounded rel n m)
Equations

- Std.Time.Internal.Bounded.instLE = { le := fun (l r : Std.Time.Internal.Bounded rel n m) => l.val ≤ r.val }

source
@[always_inline]
instance Std.Time.Internal.Bounded.instLT {rel : Int → Int → Prop} {n m : Int} :
_root_.LT (Bounded rel n m)
Equations

- Std.Time.Internal.Bounded.instLT = { lt := fun (l r : Std.Time.Internal.Bounded rel n m) => l.val < r.val }

source
@[always_inline]
instance Std.Time.Internal.Bounded.instOrd {rel : Int → Int → Prop} {n m : Int} :
Ord (Bounded rel n m)
Equations

- Std.Time.Internal.Bounded.instOrd = { compare := compareOn fun (x : Std.Time.Internal.Bounded rel n m) => x.val }

source
@[always_inline]
instance Std.Time.Internal.Bounded.instRepr {rel : Int → Int → Prop} {m n : Int} :
Repr (Bounded rel m n)
Equations

- Std.Time.Internal.Bounded.instRepr = { reprPrec := fun (n_1 : Std.Time.Internal.Bounded rel m n) => reprPrec n_1.val }

source
@[always_inline]
instance Std.Time.Internal.Bounded.instDecidableEq {rel : Int → Int → Prop} {n m : Int} :
DecidableEq (Bounded rel n m)
Equations

- Std.Time.Internal.Bounded.instDecidableEq = Subtype.instDecidableEq

source
@[always_inline]
instance Std.Time.Internal.Bounded.instDecidableLe {rel : Int → Int → Prop} {a b : Int} {x y : Bounded rel a b} :
Decidable (x ≤ y)
Equations

- Std.Time.Internal.Bounded.instDecidableLe = inferInstanceAs (Decidable (x.val ≤ y.val))

source
instance Std.Time.Internal.Bounded.instOrientedOrd {rel : Int → Int → Prop} {n m : Int} :
OrientedOrd (Bounded rel n m)
source
instance Std.Time.Internal.Bounded.instTransOrd {rel : Int → Int → Prop} {n m : Int} :
TransOrd (Bounded rel n m)
source
instance Std.Time.Internal.Bounded.instLawfulEqOrd {rel : Int → Int → Prop} {n m : Int} :
LawfulEqOrd (Bounded rel n m)
source
@[reducible, inline]
abbrev Std.Time.Internal.Bounded.LE (lo hi : Int) :
Type

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

Equations

- Std.Time.Internal.Bounded.LE = Std.Time.Internal.Bounded LE.le

Instances For

source
@[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.

Equations

- Std.Time.Internal.Bounded.cast h₁ h₂ b = ⟨b.val, ⋯⟩

Instances For

source
@[reducible, inline]
abbrev Std.Time.Internal.Bounded.LT (lo hi : Int) :
Type

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

Equations

- Std.Time.Internal.Bounded.LT = Std.Time.Internal.Bounded LT.lt

Instances For

source
@[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.

Equations

- Std.Time.Internal.Bounded.mk val proof = ⟨val, proof⟩

Instances For

source
@[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.

Equations

- Std.Time.Internal.Bounded.ofInt? val = if h : rel lo val ∧ rel val hi then some ⟨val, h⟩ else none

Instances For

source
@[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.

Equations

- Std.Time.Internal.Bounded.LE.ofNatWrapping val h = ⟨((val - lo) % (hi - lo + 1) + (hi - lo + 1)) % (hi - lo + 1) + lo, ⋯⟩

Instances For

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

- Std.Time.Internal.Bounded.LE.instOfNatHAddIntCast = { ofNat := have h := ⋯; Std.Time.Internal.Bounded.LE.ofNatWrapping (↑n) h }

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

- Std.Time.Internal.Bounded.LE.instInhabitedHAddIntCast = { default := have h := ⋯; Std.Time.Internal.Bounded.LE.ofNatWrapping lo h }

source
@[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.

Equations

- Std.Time.Internal.Bounded.LE.mk val proof = ⟨val, proof⟩

Instances For

source
@[inline]
def Std.Time.Internal.Bounded.LE.exact (val : Nat) :
LE ↑val ↑val

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

Equations

- Std.Time.Internal.Bounded.LE.exact val = ⟨↑val, ⋯⟩

Instances For

source
@[inline]
def Std.Time.Internal.Bounded.LE.ofInt {lo hi : Int} (val : Int) :
Option (LE lo hi)

Creates a new `Bounded` integer.

Equations

- Std.Time.Internal.Bounded.LE.ofInt val = if h : lo ≤ val ∧ val ≤ hi then some ⟨val, h⟩ else none

Instances For

source
@[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`.

Equations

- Std.Time.Internal.Bounded.LE.ofNat val h = Std.Time.Internal.Bounded.mk ↑val ⋯

Instances For

source
@[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.

Equations

- Std.Time.Internal.Bounded.LE.ofNat? val = if h : val ≤ hi then some (Std.Time.Internal.Bounded.LE.ofNat val h) else none

Instances For

source
@[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.

Equations

- Std.Time.Internal.Bounded.LE.ofNat' val h = Std.Time.Internal.Bounded.mk ↑val ⋯

Instances For

source
@[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.

Equations

- Std.Time.Internal.Bounded.LE.clip val h = if h₀ : lo ≤ val then if h₁ : val ≤ hi then ⟨val, ⋯⟩ else ⟨hi, ⋯⟩ else ⟨lo, ⋯⟩

Instances For

source
@[inline]
def Std.Time.Internal.Bounded.LE.toNat {lo hi : Int} (n : LE lo hi) :
Nat

Convert a `Bounded.LE` to a Nat.

Equations

- n.toNat = n.val.toNat

Instances For

source
@[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.

Equations

- n.toNat' h = match n.val, ⋯ with | Int.ofNat n, x => n | Int.negSucc a, h => ⋯.elim

Instances For

source
@[inline]
def Std.Time.Internal.Bounded.LE.toInt {lo hi : Int} (n : LE lo hi) :
Int

Convert a `Bounded.LE` to an Int.

Equations

- n.toInt = n.val

Instances For

source
@[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`.

Equations

- n.toFin h₀ = ⟨n.val.toNat, ⋯⟩

Instances For

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

Convert a `Fin` to a `Bounded.LE`.

Equations

- Std.Time.Internal.Bounded.LE.ofFin fin = Std.Time.Internal.Bounded.LE.ofNat ↑fin ⋯

Instances For

source
@[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`.

Equations

- Std.Time.Internal.Bounded.LE.ofFin' fin h = if h₁ : ↑fin ≥ lo then Std.Time.Internal.Bounded.LE.ofNat' ↑fin ⋯ else Std.Time.Internal.Bounded.LE.ofNat' lo ⋯

Instances For

source
@[inline]
def Std.Time.Internal.Bounded.LE.byEmod (b i : Int) (hi : i > 0) :
LE 0 (i - 1)

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

Equations

- Std.Time.Internal.Bounded.LE.byEmod b i hi = ⟨b % i, ⋯⟩

Instances For

source
@[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 a the Truncating modulus of a number.

Equations

- Std.Time.Internal.Bounded.LE.byMod b i hi = ⟨b.tmod i, ⋯⟩

Instances For

source
@[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).

Equations

- bounded.truncate = match ⋯ with | ⋯ => ⟨bounded.val - n, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.truncateTop h = ⟨bounded.val, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.truncateBottom h = ⟨bounded.val, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.neg = ⟨-bounded.val, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.add num = ⟨bounded.val + num, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.addProven h₀ h₁ = ⟨bounded.val + num, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.addTop num h = ⟨bounded.val + num, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.subBottom num h = ⟨bounded.val - num, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.addBounds bounded₂ = ⟨bounded.val + bounded₂.val, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.sub num = bounded.add (-num)

Instances For

source
@[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.

Equations

- bounded.subBounds bounded₂ = bounded.addBounds bounded₂.neg

Instances For

source
@[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.

Equations

- bounded.emod num hi = Std.Time.Internal.Bounded.LE.byEmod bounded.val num hi

Instances For

source
@[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.

Equations

- bounded.mod num hi = Std.Time.Internal.Bounded.LE.byMod bounded.val num hi

Instances For

source
@[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.

Equations

- bounded.mul_pos num h = ⟨bounded.val * num, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.mul_neg num h = ⟨bounded.val * num, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.ediv num h = match ⋯ with | ⋯ => ⟨bounded.val.ediv num, ⋯⟩

Instances For

source
@[inline]
def Std.Time.Internal.Bounded.LE.eq {n : Int} :
LE n n
Equations

- Std.Time.Internal.Bounded.LE.eq = ⟨n, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.expand h h₁ = ⟨bounded.val, ⋯⟩

Instances For

source
@[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.

Equations

- bounded.expandTop h = bounded.expand h ⋯

Instances For

source
@[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.

Equations

- bounded.expandBottom h = bounded.expand ⋯ h

Instances For

source
@[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.

Equations

- bounded.succ h = ⟨bounded.val + 1, ⋯⟩

Instances For

source
@[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`.

Equations

- bo.abs = if h : bo.val ≥ 0 then bo.truncateBottom h else have r := (bo.truncateTop ⋯).neg; ⋯.mp r

Instances For

source
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.

Equations

- bounded.max val = match ⋯ with | ⋯ => ⟨max bounded.val val, ⋯⟩

Instances For