def Std.Time.Minute.Ordinal : Type

Ordinal represents a bounded value for minutes, ranging from 0 to 59. This is useful for representing the minute component of a time.

Equations

• Std.Time.Minute.Ordinal = Std.Time.Internal.Bounded.LE 0 59

Instances For

• Std.Time.Minute.instInhabitedOrdinal
• Std.Time.Minute.instLawfulEqOrdOrdinal
• Std.Time.Minute.instOfNatOrdinal
• Std.Time.Minute.instOrdOrdinal
• Std.Time.Minute.instOrdinalLE
• Std.Time.Minute.instOrdinalLT
• Std.Time.Minute.instOrdinalRepr
• Std.Time.Minute.instTransOrdOrdinal

instance Std.Time.Minute.instOrdinalRepr : Repr Ordinal

Equations

• Std.Time.Minute.instOrdinalRepr = Std.Time.Internal.Bounded.instRepr

instance Std.Time.Minute.instOrdinalDecidableEq : DecidableEq Ordinal

Equations

• Std.Time.Minute.instOrdinalDecidableEq = Std.Time.Internal.Bounded.instDecidableEq

instance Std.Time.Minute.instOrdinalLE : LE Ordinal

Equations

• Std.Time.Minute.instOrdinalLE = Std.Time.Internal.Bounded.instLE

instance Std.Time.Minute.instOrdinalLT : LT Ordinal

Equations

• Std.Time.Minute.instOrdinalLT = Std.Time.Internal.Bounded.instLT

instance Std.Time.Minute.instOfNatOrdinal {n : Nat} : OfNat Ordinal n

Equations

• Std.Time.Minute.instOfNatOrdinal = inferInstanceAs (OfNat (Std.Time.Internal.Bounded.LE 0 (0 + ↑59)) n)

instance Std.Time.Minute.instInhabitedOrdinal : Inhabited Ordinal

Equations

• Std.Time.Minute.instInhabitedOrdinal = { default := 0 }

instance Std.Time.Minute.instDecidableLeOrdinal {x y : Ordinal} : Decidable (x ≤ y)

Equations

• Std.Time.Minute.instDecidableLeOrdinal = inferInstanceAs (Decidable (x.val ≤ y.val))

instance Std.Time.Minute.instDecidableLtOrdinal {x y : Ordinal} : Decidable (x < y)

Equations

• Std.Time.Minute.instDecidableLtOrdinal = inferInstanceAs (Decidable (x.val < y.val))

instance Std.Time.Minute.instOrdOrdinal : Ord Ordinal

Equations

• Std.Time.Minute.instOrdOrdinal = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 0 59))

instance Std.Time.Minute.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Minute.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

def Std.Time.Minute.Offset : Type

Offset represents a duration offset in minutes.

Equations

• Std.Time.Minute.Offset = Std.Time.Internal.UnitVal 60

Instances For

• Std.Time.DateTime.instHAddOffset_3
• Std.Time.DateTime.instHSubOffset_3
• Std.Time.Duration.instCoeOffset_2
• Std.Time.Duration.instHAddOffset_3
• Std.Time.Duration.instHSubOffset_3
• Std.Time.Minute.instLawfulEqOrdOffset
• Std.Time.Minute.instOfNatOffset
• Std.Time.Minute.instOffsetAdd
• Std.Time.Minute.instOffsetInhabited
• Std.Time.Minute.instOffsetLE
• Std.Time.Minute.instOffsetLT
• Std.Time.Minute.instOffsetNeg
• Std.Time.Minute.instOffsetRepr
• Std.Time.Minute.instOffsetSub
• Std.Time.Minute.instOffsetToString
• Std.Time.Minute.instOrdOffset
• Std.Time.Minute.instTransOrdOffset
• Std.Time.PlainDateTime.instHAddOffset_3
• Std.Time.PlainDateTime.instHSubOffset_3
• Std.Time.PlainTime.instHAddOffset_3
• Std.Time.PlainTime.instHSubOffset_3
• Std.Time.Timestamp.instHAddOffset_3
• Std.Time.Timestamp.instHSubOffset_3
• Std.Time.ZonedDateTime.instHAddOffset_3
• Std.Time.ZonedDateTime.instHSubOffset_3
• Std.Time.instHAddOffsetOffset_14
• Std.Time.instHAddOffsetOffset_18
• Std.Time.instHAddOffsetOffset_19
• Std.Time.instHAddOffsetOffset_2
• Std.Time.instHAddOffsetOffset_20
• Std.Time.instHAddOffsetOffset_21
• Std.Time.instHAddOffsetOffset_22
• Std.Time.instHAddOffsetOffset_23
• Std.Time.instHAddOffsetOffset_27
• Std.Time.instHAddOffsetOffset_33
• Std.Time.instHAddOffsetOffset_39
• Std.Time.instHAddOffsetOffset_8
• Std.Time.instHAddOffset_3
• Std.Time.instHSubOffsetOffset_14
• Std.Time.instHSubOffsetOffset_18
• Std.Time.instHSubOffsetOffset_19
• Std.Time.instHSubOffsetOffset_2
• Std.Time.instHSubOffsetOffset_20
• Std.Time.instHSubOffsetOffset_21
• Std.Time.instHSubOffsetOffset_22
• Std.Time.instHSubOffsetOffset_23
• Std.Time.instHSubOffsetOffset_27
• Std.Time.instHSubOffsetOffset_33
• Std.Time.instHSubOffsetOffset_39
• Std.Time.instHSubOffsetOffset_8
• Std.Time.instHSubOffset_3

instance Std.Time.Minute.instOffsetRepr : Repr Offset

Equations

• Std.Time.Minute.instOffsetRepr = Std.Time.Internal.UnitVal.instRepr

instance Std.Time.Minute.instOffsetDecidableEq : DecidableEq Offset

Equations

• Std.Time.Minute.instOffsetDecidableEq = Std.Time.Internal.instDecidableEqUnitVal

instance Std.Time.Minute.instOffsetInhabited : Inhabited Offset

Equations

• Std.Time.Minute.instOffsetInhabited = Std.Time.Internal.instInhabitedUnitVal

instance Std.Time.Minute.instOffsetAdd : Add Offset

Equations

• Std.Time.Minute.instOffsetAdd = Std.Time.Internal.UnitVal.instAdd

instance Std.Time.Minute.instOffsetSub : Sub Offset

Equations

• Std.Time.Minute.instOffsetSub = Std.Time.Internal.UnitVal.instSub

instance Std.Time.Minute.instOffsetNeg : Neg Offset

Equations

• Std.Time.Minute.instOffsetNeg = Std.Time.Internal.UnitVal.instNeg

instance Std.Time.Minute.instOffsetToString : ToString Offset

Equations

• Std.Time.Minute.instOffsetToString = Std.Time.Internal.UnitVal.instToString

instance Std.Time.Minute.instOffsetLT : LT Offset

Equations

• Std.Time.Minute.instOffsetLT = Std.Time.Internal.UnitVal.instLT

instance Std.Time.Minute.instOffsetLE : LE Offset

Equations

• Std.Time.Minute.instOffsetLE = Std.Time.Internal.UnitVal.instLE

instance Std.Time.Minute.instDecidableLeOffset {x y : Offset} : Decidable (x ≤ y)

Equations

• Std.Time.Minute.instDecidableLeOffset = inferInstanceAs (Decidable (x.val ≤ y.val))

instance Std.Time.Minute.instDecidableLtOffset {x y : Offset} : Decidable (x < y)

Equations

• Std.Time.Minute.instDecidableLtOffset = inferInstanceAs (Decidable (x.val < y.val))

instance Std.Time.Minute.instOfNatOffset {n : Nat} : OfNat Offset n

Equations

• Std.Time.Minute.instOfNatOffset = { ofNat := { val := Int.ofNat n } }

instance Std.Time.Minute.instOrdOffset : Ord Offset

Equations

• Std.Time.Minute.instOrdOffset = inferInstanceAs (Ord (Std.Time.Internal.UnitVal 60))

instance Std.Time.Minute.instTransOrdOffset : TransOrd Offset

instance Std.Time.Minute.instLawfulEqOrdOffset : LawfulEqOrd Offset

@[inline]

def Std.Time.Minute.Ordinal.ofInt (data : Int) (h : 0 ≤ data ∧ data ≤ 59) : Ordinal

Creates an Ordinal from an integer, ensuring the value is within bounds.

Equations

• Std.Time.Minute.Ordinal.ofInt data h = Std.Time.Internal.Bounded.LE.mk data h

@[inline]

def Std.Time.Minute.Ordinal.ofNat (data : Nat) (h : data ≤ 59) : Ordinal

Creates an Ordinal from a natural number, ensuring the value is within bounds.

Equations

• Std.Time.Minute.Ordinal.ofNat data h = Std.Time.Internal.Bounded.LE.ofNat data h

@[inline]

def Std.Time.Minute.Ordinal.ofFin (data : Fin 60) : Ordinal

Creates an Ordinal from a Fin, ensuring the value is within bounds.

Equations

• Std.Time.Minute.Ordinal.ofFin data = Std.Time.Internal.Bounded.LE.ofFin data

@[inline]

def Std.Time.Minute.Ordinal.toOffset (ordinal : Ordinal) : Offset

Converts an Ordinal to an Offset.

Equations

• ordinal.toOffset = { val := ordinal.val }

@[inline]

def Std.Time.Minute.Offset.ofNat (data : Nat) : Offset

Creates an Offset from a natural number.

Equations

• Std.Time.Minute.Offset.ofNat data = { val := ↑data }

@[inline]

def Std.Time.Minute.Offset.ofInt (data : Int) : Offset

Creates an Offset from an integer.

Equations

• Std.Time.Minute.Offset.ofInt data = { val := data }