Data.Time.Time

Reexports

Definitions

record Hour : Type

Totality: total
Visibility: public export
Constructor: 

H : (hour : Integer) -> {auto 0 _ : FromTo 0 23 hour} -> Hour

Projections:

.hour : Hour -> Integer

0 .valid : ({rec:0} : Hour) -> FromTo 0 23 (hour {rec:0})

Hints:

Eq Hour

Interpolation Hour

Ord Hour

Show Hour

.hour : Hour -> Integer

Totality: total
Visibility: public export

hour : Hour -> Integer

Totality: total
Visibility: public export

0 .valid : ({rec:0} : Hour) -> FromTo 0 23 (hour {rec:0})

Totality: total
Visibility: public export

0 valid : ({rec:0} : Hour) -> FromTo 0 23 (hour {rec:0})

Totality: total
Visibility: public export

record Minute : Type

Totality: total
Visibility: public export
Constructor: 

M : (minute : Integer) -> {auto 0 _ : FromTo 0 59 minute} -> Minute

Projections:

.minute : Minute -> Integer

0 .valid : ({rec:0} : Minute) -> FromTo 0 59 (minute {rec:0})

Hints:

Eq Minute

Interpolation Minute

Ord Minute

Show Minute

.minute : Minute -> Integer

Totality: total
Visibility: public export

minute : Minute -> Integer

Totality: total
Visibility: public export

0 .valid : ({rec:0} : Minute) -> FromTo 0 59 (minute {rec:0})

Totality: total
Visibility: public export

0 valid : ({rec:0} : Minute) -> FromTo 0 59 (minute {rec:0})

Totality: total
Visibility: public export

record Second : Type

Totality: total
Visibility: public export
Constructor: 

S : (second : Integer) -> {auto 0 _ : FromTo 0 60 second} -> Second

Projections:

.second : Second -> Integer

0 .valid : ({rec:0} : Second) -> FromTo 0 60 (second {rec:0})

Hints:

Eq Second

Interpolation Second

Ord Second

Show Second

.second : Second -> Integer

Totality: total
Visibility: public export

second : Second -> Integer

Totality: total
Visibility: public export

0 .valid : ({rec:0} : Second) -> FromTo 0 60 (second {rec:0})

Totality: total
Visibility: public export

0 valid : ({rec:0} : Second) -> FromTo 0 60 (second {rec:0})

Totality: total
Visibility: public export

record MicroSecond : Type

Totality: total
Visibility: public export
Constructor: 

MS : (us : Integer) -> {auto 0 _ : FromTo 0 999999 us} -> MicroSecond

Projections:

.us : MicroSecond -> Integer

0 .valid : ({rec:0} : MicroSecond) -> FromTo 0 999999 (us {rec:0})

Hints:

Eq MicroSecond

Interpolation MicroSecond

Ord MicroSecond

Show MicroSecond

.us : MicroSecond -> Integer

Totality: total
Visibility: public export

us : MicroSecond -> Integer

Totality: total
Visibility: public export

0 .valid : ({rec:0} : MicroSecond) -> FromTo 0 999999 (us {rec:0})

Totality: total
Visibility: public export

0 valid : ({rec:0} : MicroSecond) -> FromTo 0 999999 (us {rec:0})

Totality: total
Visibility: public export

record LocalTime : Type

Totality: total
Visibility: public export
Constructor: 

LT : Hour -> Minute -> Second -> Maybe MicroSecond -> LocalTime

Projections:

.hour : LocalTime -> Hour

.minute : LocalTime -> Minute

.prec : LocalTime -> Maybe MicroSecond

.second : LocalTime -> Second

Hints:

Eq LocalTime

Interpolation LocalTime

Ord LocalTime

Show LocalTime

.hour : LocalTime -> Hour

Totality: total
Visibility: public export

hour : LocalTime -> Hour

Totality: total
Visibility: public export

.minute : LocalTime -> Minute

Totality: total
Visibility: public export

minute : LocalTime -> Minute

Totality: total
Visibility: public export

.second : LocalTime -> Second

Totality: total
Visibility: public export

second : LocalTime -> Second

Totality: total
Visibility: public export

.prec : LocalTime -> Maybe MicroSecond

Totality: total
Visibility: public export

prec : LocalTime -> Maybe MicroSecond

Totality: total
Visibility: public export

data Sign : Type

Totality: total
Visibility: public export
Constructors:

Minus : Sign

Plus : Sign

Hints:

Eq Sign

Interpolation Sign

Ord Sign

Show Sign

data Offset : Type

Totality: total
Visibility: public export
Constructors:

Z : Offset

O : Sign -> Hour -> Minute -> Offset

Hints:

Eq Offset

Interpolation Offset

Show Offset

record OffsetTime : Type

Totality: total
Visibility: public export
Constructor: 

OT : LocalTime -> Offset -> OffsetTime

Projections:

.offset : OffsetTime -> Offset

.time : OffsetTime -> LocalTime

Hints:

Eq OffsetTime

Interpolation OffsetTime

Show OffsetTime

.time : OffsetTime -> LocalTime

Totality: total
Visibility: public export

time : OffsetTime -> LocalTime

Totality: total
Visibility: public export

.offset : OffsetTime -> Offset

Totality: total
Visibility: public export

offset : OffsetTime -> Offset

Totality: total
Visibility: public export

record LocalDateTime : Type

Totality: total
Visibility: public export
Constructor: 

LDT : Date -> LocalTime -> LocalDateTime

Projections:

.date : LocalDateTime -> Date

.time : LocalDateTime -> LocalTime

Hints:

Eq LocalDateTime

Interpolation LocalDateTime

Show LocalDateTime

.date : LocalDateTime -> Date

Totality: total
Visibility: public export

date : LocalDateTime -> Date

Totality: total
Visibility: public export

.time : LocalDateTime -> LocalTime

Totality: total
Visibility: public export

time : LocalDateTime -> LocalTime

Totality: total
Visibility: public export

record OffsetDateTime : Type

Totality: total
Visibility: public export
Constructor: 

ODT : Date -> OffsetTime -> OffsetDateTime

Projections:

.date : OffsetDateTime -> Date

.time : OffsetDateTime -> OffsetTime

Hints:

Eq OffsetDateTime

Interpolation OffsetDateTime

Show OffsetDateTime

.date : OffsetDateTime -> Date

Totality: total
Visibility: public export

date : OffsetDateTime -> Date

Totality: total
Visibility: public export

.time : OffsetDateTime -> OffsetTime

Totality: total
Visibility: public export

time : OffsetDateTime -> OffsetTime

Totality: total
Visibility: public export

data AnyTime : Type

Totality: total
Visibility: public export
Constructors:

ATDate : Date -> AnyTime

ATLocalTime : LocalTime -> AnyTime

ATLocalDateTime : LocalDateTime -> AnyTime

ATOffsetDateTime : OffsetDateTime -> AnyTime

Hints:

Eq AnyTime

Interpolation AnyTime

Show AnyTime