A structure representing a unit of a given ratio type α
.
- ofInt :: (
- val : Int
Value inside the UnitVal Value.
- )
Instances For
- Std.Time.Internal.UnitVal.instAdd
- Std.Time.Internal.UnitVal.instLE
- Std.Time.Internal.UnitVal.instLT
- Std.Time.Internal.UnitVal.instNeg
- Std.Time.Internal.UnitVal.instOfNat
- Std.Time.Internal.UnitVal.instRepr
- Std.Time.Internal.UnitVal.instSub
- Std.Time.Internal.UnitVal.instToString
- Std.Time.Internal.instBEqUnitVal
- Std.Time.Internal.instInhabitedUnitVal
- Std.Time.Internal.instLEUnitVal
Equations
- Std.Time.Internal.instInhabitedUnitVal = { default := { val := default } }
Equations
Equations
- Std.Time.Internal.instLEUnitVal = { le := fun (x_1 y : Std.Time.Internal.UnitVal x) => x_1.val ≤ y.val }
Equations
- Std.Time.Internal.instDecidableLeUnitVal = inferInstanceAs (Decidable (x.val ≤ y.val))
@[inline]
Equations
- Std.Time.Internal.UnitVal.ofNat value = { val := ↑value }
@[inline]
Equations
- unit.toInt = unit.val
@[inline]
Adds two UnitVal
values of the same ratio.
@[inline]
Subtracts one UnitVal
value from another of the same ratio.
@[inline]
Converts an Offset
to another unit type.
Equations
- Std.Time.Internal.UnitVal.instOfNat = { ofNat := { val := Int.ofNat n } }
Equations
- Std.Time.Internal.UnitVal.instRepr = { reprPrec := fun (x : Std.Time.Internal.UnitVal α) (p : Nat) => reprPrec x.val p }
Equations
- Std.Time.Internal.UnitVal.instLE = { le := fun (x y : Std.Time.Internal.UnitVal α) => x.val ≤ y.val }
Equations
- Std.Time.Internal.UnitVal.instLT = { lt := fun (x y : Std.Time.Internal.UnitVal α) => x.val < y.val }
Equations
Equations
Equations
- Std.Time.Internal.UnitVal.instNeg = { neg := fun (x : Std.Time.Internal.UnitVal α) => { val := -x.val } }
Equations
- Std.Time.Internal.UnitVal.instToString = { toString := fun (n_1 : Std.Time.Internal.UnitVal n) => toString n_1.val }