Equations
- Std.Time.Internal.Bounded.instLE = { le := fun (l r : Std.Time.Internal.Bounded rel n m) => l.val ≤ r.val }
Equations
- Std.Time.Internal.Bounded.instLT = { lt := fun (l r : Std.Time.Internal.Bounded rel n m) => l.val < r.val }
A Bounded
integer that the relation used is the the less-equal relation so, it includes all
integers that lo ≤ val ≤ hi
.
Equations
Casts the boundaries of the Bounded
using equivalences.
Equations
- Std.Time.Internal.Bounded.cast h₁ h₂ b = ⟨b.val, ⋯⟩
A Bounded
integer that the relation used is the the less-than relation so, it includes all
integers that lo < val < hi
.
Creates a new Bounded
Integer.
Equations
- Std.Time.Internal.Bounded.mk val proof = ⟨val, proof⟩
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
Convert a Nat
to a Bounded.LE
by wrapping it.
Equations
- Std.Time.Internal.Bounded.LE.instOfNatHAddIntCast = { ofNat := let h := ⋯; Std.Time.Internal.Bounded.LE.ofNatWrapping (↑n) h }
Equations
- Std.Time.Internal.Bounded.LE.instInhabitedHAddIntCast = { default := let h := ⋯; Std.Time.Internal.Bounded.LE.ofNatWrapping lo h }
Creates a new Bounded
integer that the relation is less-equal.
Equations
- Std.Time.Internal.Bounded.LE.mk val proof = ⟨val, proof⟩
Creates a new Bounded
integer that the relation is less-equal.
Creates a new Bounded
integer.
Convert a Nat
to a Bounded.LE
.
Equations
Convert a Nat
to a Bounded.LE
if it checks.
Convert a Nat
to a Bounded.LE
using the lower boundary too.
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, ⋯⟩
Convert a Bounded.LE
to a Nat.
Convert a Bounded.LE
to a Nat.
Convert a Bounded.LE
to a Fin
.
Equations
- n.toFin h₀ = ⟨n.val.toNat, ⋯⟩
Convert a Fin
to a Bounded.LE
.
Convert a Fin
to a Bounded.LE
.
Creates a new Bounded.LE
using a the modulus of a number.
Equations
- Std.Time.Internal.Bounded.LE.byEmod b i hi = ⟨b % i, ⋯⟩
Creates a new Bounded.LE
using a the Truncating modulus of a number.
Adjust the bounds of a Bounded
by setting the lower bound to zero and the maximum value to (m - n).
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, ⋯⟩
Adjust the bounds of a Bounded
by changing the lower bound if another value j
satisfies the same
constraint.
Adjust the bounds of a Bounded
by adding a constant value to both the lower and upper bounds.
Adjust the bounds of a Bounded
by adding a constant value to both the lower and upper bounds.
Adjust the bounds of a Bounded
by adding a constant value to both the lower and upper bounds.
Adjust the bounds of a Bounded
by adding a constant value to the upper bounds.
Adjust the bounds of a Bounded
by adding a constant value to the lower bounds.
Adds two Bounded
and adjust the boundaries.
Adjust the bounds of a Bounded
by subtracting a constant value to both the lower and upper bounds.
Adds two Bounded
and adjust the boundaries.
Equations
- bounded.subBounds bounded₂ = bounded.addBounds bounded₂.neg
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
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
Adjust the bounds of a Bounded
by applying the multiplication operation with a positive number.
Adjust the bounds of a Bounded
by applying the multiplication operation with a positive number.
Adjust the bounds of a Bounded
by applying the div operation.
Equations
- bounded.ediv num h = match ⋯ with | ⋯ => ⟨bounded.val.ediv num, ⋯⟩
Equations
- Std.Time.Internal.Bounded.LE.eq = ⟨n, ⋯⟩
Expand the range of a bounded value.
Equations
- bounded.expand h h₁ = ⟨bounded.val, ⋯⟩
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 ⋯
Expand the bottom of the bounded to a number nlo
if lo
is greater or equal to the previous lower bound.
Adds one to the value of the bounded if the value is less than the higher bound of the bounded number.
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
.
Returns the maximum between a number and the bounded.