Std.Time.Internal.UnitVal

source

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

Type

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

ofInt :: (

val : Int
Value inside the UnitVal Value.

)

Instances For

source

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

x = y

source

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

x = y ↔ x.val = y.val

source

instance Std.Time.Internal.instInhabitedUnitVal {a✝ : Internal.Rat} :

Inhabited (UnitVal a✝)

Equations

source

instance Std.Time.Internal.instDecidableEqUnitVal {α✝ : Internal.Rat} :

DecidableEq (UnitVal α✝)

Equations

source

instance Std.Time.Internal.instLEUnitVal {x : Internal.Rat} :

LE (UnitVal x)

Equations

source

instance Std.Time.Internal.instOrdUnitVal {x : Internal.Rat} :

Ord (UnitVal x)

Equations

source

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

compare a b = compare a.val b.val

source

instance Std.Time.Internal.instOrientedOrdUnitVal {x : Internal.Rat} :

OrientedOrd (UnitVal x)

source

instance Std.Time.Internal.instTransOrdUnitVal {x : Internal.Rat} :

TransOrd (UnitVal x)

source

instance Std.Time.Internal.instLawfulEqOrdUnitVal {x : Internal.Rat} :

LawfulEqOrd (UnitVal x)

source

instance Std.Time.Internal.instDecidableLeUnitVal {z : Internal.Rat} {x y : UnitVal z} :

Decidable (x ≤ y)

Equations

source

@[inline]

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

UnitVal α

Creates a UnitVal from a Nat.

Equations

Instances For

source

@[inline]

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

Int

Converts a UnitVal to an Int.

Equations

Instances For

source

@[inline]

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

UnitVal (a / { num := factor })

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

Equations

Instances For

source

@[inline]

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

UnitVal (a * { num := divisor })

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

Equations

Instances For

source

@[inline]

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

UnitVal (a * { num := divisor })

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

Equations

Instances For

source

@[inline]

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

UnitVal (a * { num := divisor })

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

Equations

Instances For

source

@[inline]

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

UnitVal α

Adds two UnitVal values of the same ratio.

Equations

Instances For

source

@[inline]

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

UnitVal α

Subtracts one UnitVal value from another of the same ratio.

Equations

Instances For

source

@[inline]

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

UnitVal α

Returns the absolute value of a UnitVal.

Equations

Instances For

source

@[inline]

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

UnitVal b

Converts an Offset to another unit type.

Equations

Instances For

source

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

OfNat (UnitVal α) n

Equations

source

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

Repr (UnitVal α)

Equations

source

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

LE (UnitVal α)

Equations

source

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

LT (UnitVal α)

Equations

source

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

Add (UnitVal α)

Equations

source

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

Sub (UnitVal α)

Equations

source

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

Neg (UnitVal α)

Equations

source

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

ToString (UnitVal n)

Equations