@[always_inline]
instance
Std.Time.Internal.Bounded.instDecidableEq
{rel : Int → Int → Prop}
{n m : Int}
:
DecidableEq (Bounded rel n m)
Equations
instance
Std.Time.Internal.Bounded.instOrientedOrd
{rel : Int → Int → Prop}
{n m : Int}
:
OrientedOrd (Bounded rel n m)
instance
Std.Time.Internal.Bounded.instLawfulEqOrd
{rel : Int → Int → Prop}
{n m : Int}
:
LawfulEqOrd (Bounded rel n m)
@[reducible, inline]
A Bounded
integer that the relation used is the the less-equal relation so, it includes all
integers that lo ≤ val ≤ hi
.
Equations
Instances For
@[reducible, inline]
A Bounded
integer that the relation used is the the less-than relation so, it includes all
integers that lo < val < hi
.
Equations
Instances For
@[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
Instances For
@[inline]
Convert a Bounded.LE
to a Fin
.
Equations
Instances For
@[inline]
Creates a new Bounded.LE
using a the Truncating modulus of a number.