Documentation

Std.Time.Internal.UnitVal

@[inline]

Creates a UnitVal from a Nat.

Equations
@[inline]

Converts a UnitVal to an Int.

Equations
  • unit.toInt = unit.val
@[inline]
def Std.Time.Internal.UnitVal.mul {a : Internal.Rat} (unit : UnitVal a) (factor : Int) :
UnitVal (a / { num := factor, den := 1 })

Multiplies the UnitVal by an Int, resulting in a new UnitVal with an adjusted ratio.

Equations
  • unit.mul factor = { val := unit.val * factor }
@[inline]
def Std.Time.Internal.UnitVal.ediv {a : Internal.Rat} (unit : UnitVal a) (divisor : Int) :
UnitVal (a * { num := divisor, den := 1 })

Divides the UnitVal by an Int, resulting in a new UnitVal with an adjusted ratio.

Equations
  • unit.ediv divisor = { val := unit.val.ediv divisor }
@[inline]
def Std.Time.Internal.UnitVal.div {a : Internal.Rat} (unit : UnitVal a) (divisor : Int) :
UnitVal (a * { num := divisor, den := 1 })

Divides the UnitVal by an Int, resulting in a new UnitVal with an adjusted ratio.

Equations
  • unit.div divisor = { val := unit.val.tdiv divisor }
@[inline]

Adds two UnitVal values of the same ratio.

Equations
  • u1.add u2 = { val := u1.val + u2.val }
@[inline]

Subtracts one UnitVal value from another of the same ratio.

Equations
  • u1.sub u2 = { val := u1.val - u2.val }
@[inline]

Returns the absolute value of a UnitVal.

Equations
  • u.abs = { val := u.val.natAbs }
@[inline]

Converts an Offset to another unit type.

Equations
  • val.convert = { val := val.toInt * (a.div b).num / (a.div b).den }