IotaTime.LocalTime

Reexports

Definitions

record LocalTime : Type

  An opaque time of day with nanosecond precision.

Totality: total
Visibility: export
Constructor: 

MkLocalTime : Integer -> LocalTime

Projection: 

.nanosSinceMidnight : LocalTime -> Integer

Hints:

ApplyPeriod LocalTime

Eq LocalTime

HasTime LocalTime

Ord LocalTime

PeriodTarget LocalTime

Show LocalTime

toNanosecondsSinceMidnight : LocalTime -> Integer

Totality: total
Visibility: export

localTime : Hour -> Minute -> Second -> Nanosecond -> LocalTime

  Construct a local time from already refined components.

Totality: total
Visibility: public export

hour : LocalTime -> Hour

  Extract the hour in the range 0-23.

Totality: total
Visibility: public export

minute : LocalTime -> Minute

  Extract the minute in the range 0-59.

Totality: total
Visibility: public export

second : LocalTime -> Second

  Extract the second in the range 0-59.

Totality: total
Visibility: public export

nanosecond : LocalTime -> Nanosecond

  Extract the nanosecond within the current second.

Totality: total
Visibility: public export

data LocalTimeError : Type

  Identifies which raw local-time component failed refinement.

Totality: total
Visibility: public export
Constructors:

InvalidHour : HourError -> LocalTimeError

InvalidMinute : MinuteError -> LocalTimeError

InvalidSecond : SecondError -> LocalTimeError

InvalidNanosecond : NanosecondError -> LocalTimeError

refineLocalTime : Integer -> Integer -> Integer -> Integer -> Either LocalTimeError LocalTime

  Validate raw hour, minute, second, and nanosecond values as a local time.

Totality: total
Visibility: public export

applyTimePeriodWithCarry : Period target -> LocalTime -> (Integer, LocalTime)

Totality: total
Visibility: export

between : LocalTime -> LocalTime -> Period LocalTime

  Compute the signed same-day period from `start` to `end`.
  No implicit midnight crossing is chosen: an earlier `end` produces a
  negative period.

Totality: total
Visibility: public export