structure Std.Time.Internal.UnitVal (α : Std.Internal.Rat) : Type

A structure representing a unit of a given ratio type α.

• ofInt :: (
• val : Int

  Value inside the UnitVal Value.

• )

instance Std.Time.Internal.instInhabitedUnitVal {a✝ : Std.Internal.Rat} : Inhabited (Std.Time.Internal.UnitVal a✝)

Equations

• Std.Time.Internal.instInhabitedUnitVal = { default := { val := default } }

instance Std.Time.Internal.instBEqUnitVal {α✝ : Std.Internal.Rat} : BEq (Std.Time.Internal.UnitVal α✝)

Equations

• Std.Time.Internal.instBEqUnitVal = { beq := Std.Time.Internal.beqUnitVal✝ }

instance Std.Time.Internal.instLEUnitVal {x : Std.Internal.Rat} : LE (Std.Time.Internal.UnitVal x)

Equations

• Std.Time.Internal.instLEUnitVal = { le := fun (x_1 y : Std.Time.Internal.UnitVal x) => x_1.val ≤ y.val }

instance Std.Time.Internal.instDecidableLeUnitVal {z : Std.Internal.Rat} {x y : Std.Time.Internal.UnitVal z} : Decidable (x ≤ y)

Equations

• Std.Time.Internal.instDecidableLeUnitVal = inferInstanceAs (Decidable (x.val ≤ y.val))

@[inline]

def Std.Time.Internal.UnitVal.ofNat {α : Std.Internal.Rat} (value : Nat) : Std.Time.Internal.UnitVal α

Creates a UnitVal from a Nat.

@[inline]

def Std.Time.Internal.UnitVal.toInt {α : Std.Internal.Rat} (unit : Std.Time.Internal.UnitVal α) : Int

Converts a UnitVal to an Int.

@[inline]

def Std.Time.Internal.UnitVal.mul {a : Std.Internal.Rat} (unit : Std.Time.Internal.UnitVal a) (factor : Int) : Std.Time.Internal.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 : Std.Internal.Rat} (unit : Std.Time.Internal.UnitVal a) (divisor : Int) : Std.Time.Internal.UnitVal (a * { num := divisor, den := 1 })

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

@[inline]

def Std.Time.Internal.UnitVal.div {a : Std.Internal.Rat} (unit : Std.Time.Internal.UnitVal a) (divisor : Int) : Std.Time.Internal.UnitVal (a * { num := divisor, den := 1 })

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

@[inline]

def Std.Time.Internal.UnitVal.add {α : Std.Internal.Rat} (u1 u2 : Std.Time.Internal.UnitVal α) : Std.Time.Internal.UnitVal α

Adds two UnitVal values of the same ratio.

Equations

• u1.add u2 = { val := u1.val + u2.val }

@[inline]

def Std.Time.Internal.UnitVal.sub {α : Std.Internal.Rat} (u1 u2 : Std.Time.Internal.UnitVal α) : Std.Time.Internal.UnitVal α

Subtracts one UnitVal value from another of the same ratio.

@[inline]

def Std.Time.Internal.UnitVal.abs {α : Std.Internal.Rat} (u : Std.Time.Internal.UnitVal α) : Std.Time.Internal.UnitVal α

Returns the absolute value of a UnitVal.

@[inline]

def Std.Time.Internal.UnitVal.convert {a b : Std.Internal.Rat} (val : Std.Time.Internal.UnitVal a) : Std.Time.Internal.UnitVal b

Converts an Offset to another unit type.

instance Std.Time.Internal.UnitVal.instOfNat {α : Std.Internal.Rat} {n : Nat} : OfNat (Std.Time.Internal.UnitVal α) n

instance Std.Time.Internal.UnitVal.instRepr {α : Std.Internal.Rat} : Repr (Std.Time.Internal.UnitVal α)

Equations

• Std.Time.Internal.UnitVal.instRepr = { reprPrec := fun (x : Std.Time.Internal.UnitVal α) (p : Nat) => reprPrec x.val p }

instance Std.Time.Internal.UnitVal.instLE {α : Std.Internal.Rat} : LE (Std.Time.Internal.UnitVal α)

Equations

• Std.Time.Internal.UnitVal.instLE = { le := fun (x y : Std.Time.Internal.UnitVal α) => x.val ≤ y.val }

instance Std.Time.Internal.UnitVal.instLT {α : Std.Internal.Rat} : LT (Std.Time.Internal.UnitVal α)

instance Std.Time.Internal.UnitVal.instAdd {α : Std.Internal.Rat} : Add (Std.Time.Internal.UnitVal α)

Equations

• Std.Time.Internal.UnitVal.instAdd = { add := Std.Time.Internal.UnitVal.add }

instance Std.Time.Internal.UnitVal.instSub {α : Std.Internal.Rat} : Sub (Std.Time.Internal.UnitVal α)

instance Std.Time.Internal.UnitVal.instNeg {α : Std.Internal.Rat} : Neg (Std.Time.Internal.UnitVal α)

instance Std.Time.Internal.UnitVal.instToString {n : Std.Internal.Rat} : ToString (Std.Time.Internal.UnitVal n)