IotaTime.Time.Component

Reexports

Definitions

isValidHour : Integer -> Bool

  Whether an integer is in the inclusive hour range 0 through 23.

Totality: total
Visibility: public export

record Hour : Type

  An hour of day constrained to the inclusive range 0 through 23.

Totality: total
Visibility: export
Constructor: 

MkHour : Integer -> Hour

Projection: 

.integerValue : Hour -> Integer

Hints:

Eq Hour

Show Hour

fromInteger : (value : Integer) -> {auto 0 _ : So (isValidHour value)} -> Hour

  Construct an hour when its range proof is available statically.

Totality: total
Visibility: public export

hourValue : Hour -> Integer

  Return the integer hour of day.

Totality: total
Visibility: public export

data HourError : Type

  A runtime hour value outside the inclusive range 0 through 23.

Totality: total
Visibility: public export
Constructor: 

HourOutOfRange : Integer -> HourError

refineHour : Integer -> Either HourError Hour

  Refine an untrusted integer into an hour or return a typed range error.

Totality: total
Visibility: public export

isValidMinute : Integer -> Bool

  Whether an integer is in the inclusive minute range 0 through 59.

Totality: total
Visibility: public export

record Minute : Type

  A minute of hour constrained to the inclusive range 0 through 59.

Totality: total
Visibility: export
Constructor: 

MkMinute : Integer -> Minute

Projection: 

.integerValue : Minute -> Integer

Hints:

Eq Minute

Show Minute

fromInteger : (value : Integer) -> {auto 0 _ : So (isValidMinute value)} -> Minute

  Construct a minute when its range proof is available statically.

Totality: total
Visibility: public export

minuteValue : Minute -> Integer

  Return the integer minute of hour.

Totality: total
Visibility: public export

data MinuteError : Type

  A runtime minute value outside the inclusive range 0 through 59.

Totality: total
Visibility: public export
Constructor: 

MinuteOutOfRange : Integer -> MinuteError

refineMinute : Integer -> Either MinuteError Minute

  Refine an untrusted integer into a minute or return a typed range error.

Totality: total
Visibility: public export

isValidSecond : Integer -> Bool

  Whether an integer is in the inclusive second range 0 through 59.

Totality: total
Visibility: public export

record Second : Type

  A second of minute constrained to the inclusive range 0 through 59.

Totality: total
Visibility: export
Constructor: 

MkSecond : Integer -> Second

Projection: 

.integerValue : Second -> Integer

Hints:

Eq Second

Show Second

fromInteger : (value : Integer) -> {auto 0 _ : So (isValidSecond value)} -> Second

  Construct a second when its range proof is available statically.

Totality: total
Visibility: public export

secondValue : Second -> Integer

  Return the integer second of minute.

Totality: total
Visibility: public export

data SecondError : Type

  A runtime second value outside the inclusive range 0 through 59.

Totality: total
Visibility: public export
Constructor: 

SecondOutOfRange : Integer -> SecondError

refineSecond : Integer -> Either SecondError Second

  Refine an untrusted integer into a second or return a typed range error.

Totality: total
Visibility: public export

isValidNanosecond : Integer -> Bool

  Whether an integer is in the nanosecond range 0 through 999,999,999.

Totality: total
Visibility: public export

record Nanosecond : Type

  A nanosecond of second constrained to 0 through 999,999,999.

Totality: total
Visibility: export
Constructor: 

MkNanosecond : Integer -> Nanosecond

Projection: 

.integerValue : Nanosecond -> Integer

Hints:

Eq Nanosecond

Show Nanosecond

fromInteger : (value : Integer) -> {auto 0 _ : So (isValidNanosecond value)} -> Nanosecond

  Construct a nanosecond when its range proof is available statically.

Totality: total
Visibility: public export

nanosecondValue : Nanosecond -> Integer

  Return the integer nanosecond of second.

Totality: total
Visibility: public export

data NanosecondError : Type

  A runtime nanosecond value outside 0 through 999,999,999.

Totality: total
Visibility: public export
Constructor: 

NanosecondOutOfRange : Integer -> NanosecondError

refineNanosecond : Integer -> Either NanosecondError Nanosecond

  Refine an untrusted integer into a nanosecond or return a typed range error.

Totality: total
Visibility: public export