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

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

• ofInt :: (
• val : Int

  Value inside the UnitVal Value.

• )

theorem Std.Time.Internal.UnitVal.ext {α : Rat} {x y : UnitVal α} (val : x.val = y.val) : x = y

theorem Std.Time.Internal.UnitVal.ext_iff {α : Rat} {x y : UnitVal α} : x = y ↔ x.val = y.val

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

Equations

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

def Std.Time.Internal.instInhabitedUnitVal.default {a✝ : Rat} : UnitVal a✝

Equations

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

instance Std.Time.Internal.instDecidableEqUnitVal {α✝ : Rat} : DecidableEq (UnitVal α✝)

Equations

• Std.Time.Internal.instDecidableEqUnitVal = Std.Time.Internal.instDecidableEqUnitVal.decEq

def Std.Time.Internal.instDecidableEqUnitVal.decEq {α✝ : Rat} (x✝ x✝¹ : UnitVal α✝) : Decidable (x✝ = x✝¹)

Equations

• Std.Time.Internal.instDecidableEqUnitVal.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Std.Time.Internal.instLEUnitVal {x : Rat} : LE (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.instOrdUnitVal {x : Rat} : Ord (UnitVal x)

Equations

• Std.Time.Internal.instOrdUnitVal = { compare := fun (x_1 y : Std.Time.Internal.UnitVal x) => compare x_1.val y.val }

theorem Std.Time.Internal.UnitVal.compare_def {x : Rat} {a b : UnitVal x} : compare a b = compare a.val b.val

instance Std.Time.Internal.instOrientedOrdUnitVal {x : Rat} : OrientedOrd (UnitVal x)

instance Std.Time.Internal.instTransOrdUnitVal {x : Rat} : TransOrd (UnitVal x)

instance Std.Time.Internal.instLawfulEqOrdUnitVal {x : Rat} : LawfulEqOrd (UnitVal x)

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

Equations

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

@[inline]

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

Creates a UnitVal from a Nat.

Equations

• Std.Time.Internal.UnitVal.ofNat value = { val := ↑value }

@[inline]

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

Converts a UnitVal to an Int.

Equations

• unit.toInt = unit.val

@[inline]

def Std.Time.Internal.UnitVal.mul {a : Rat} (unit : UnitVal a) (factor : Int) : UnitVal (a / ↑factor)

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 : Rat} (unit : UnitVal a) (divisor : Int) : UnitVal (a * ↑divisor)

Divides the UnitVal by an Int, resulting in a new UnitVal with an adjusted ratio. Using the E-rounding convention (euclidean division)

Equations

• unit.ediv divisor = { val := unit.val.ediv divisor }

@[inline]

def Std.Time.Internal.UnitVal.tdiv {a : Rat} (unit : UnitVal a) (divisor : Int) : UnitVal (a * ↑divisor)

Divides the UnitVal by an Int, resulting in a new UnitVal with an adjusted ratio. Using the "T-rounding" (Truncation-rounding) convention

Equations

• unit.tdiv divisor = { val := unit.val.tdiv divisor }

@[inline]

def Std.Time.Internal.UnitVal.div {a : Rat} (unit : UnitVal a) (divisor : Int) : UnitVal (a * ↑divisor)

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]

def Std.Time.Internal.UnitVal.add {α : Rat} (u1 u2 : UnitVal α) : 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 {α : Rat} (u1 u2 : UnitVal α) : UnitVal α

Subtracts one UnitVal value from another of the same ratio.

Equations

• u1.sub u2 = { val := u1.val - u2.val }

@[inline]

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

Returns the absolute value of a UnitVal.

Equations

• u.abs = { val := ↑u.val.natAbs }

@[inline]

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

Converts an Offset to another unit type.

Equations

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

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

Equations

• Std.Time.Internal.UnitVal.instOfNat = { ofNat := { val := Int.ofNat n } }

instance Std.Time.Internal.UnitVal.instRepr {α : Rat} : Repr (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 {α : Rat} : LE (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 {α : Rat} : LT (UnitVal α)

Equations

• Std.Time.Internal.UnitVal.instLT = { lt := fun (x y : Std.Time.Internal.UnitVal α) => x.val < y.val }

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

Equations

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

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

Equations

• Std.Time.Internal.UnitVal.instSub = { sub := Std.Time.Internal.UnitVal.sub }

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

Equations

• Std.Time.Internal.UnitVal.instNeg = { neg := fun (x : Std.Time.Internal.UnitVal α) => { val := -x.val } }

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

Equations

• Std.Time.Internal.UnitVal.instToString = { toString := fun (n_1 : Std.Time.Internal.UnitVal n) => toString n_1.val }

def Std.Time.Internal.UnitVal.cast {a b : Rat} : a = b → (x : UnitVal a) → UnitVal b

Cast a UnitVal through an equality in the rational numbers.

Equations

• Std.Time.Internal.UnitVal.cast x✝ x = { val := x.val }