record Date : Type- Totality: total
Visibility: public export
Constructor: D : Integer -> Integer -> Integer -> Date
Projections:
.day : Date -> Integer.month : Date -> Integer.year : Date -> Integer
Hint: Show Date
.year : Date -> Integer- Visibility: public export
year : Date -> Integer- Visibility: public export
.month : Date -> Integer- Visibility: public export
month : Date -> Integer- Visibility: public export
.day : Date -> Integer- Visibility: public export
day : Date -> Integer- Visibility: public export
record Time : Type- Totality: total
Visibility: public export
Constructor: T : Integer -> Integer -> Integer -> Integer -> Time
Projections:
.hours : Time -> Integer.milis : Time -> Integer.min : Time -> Integer.sec : Time -> Integer
Hint: Show Time
.hours : Time -> Integer- Visibility: public export
hours : Time -> Integer- Visibility: public export
.min : Time -> Integer- Visibility: public export
min : Time -> Integer- Visibility: public export
.sec : Time -> Integer- Visibility: public export
sec : Time -> Integer- Visibility: public export
.milis : Time -> Integer- Visibility: public export
milis : Time -> Integer- Visibility: public export
record DateTime : Type- Totality: total
Visibility: public export
Constructor: DT : Date -> Time -> DateTime
Projections:
.date : DateTime -> Date.time : DateTime -> Time
Hint: Show DateTime
.date : DateTime -> Date- Visibility: public export
date : DateTime -> Date- Visibility: public export
.time : DateTime -> Time- Visibility: public export
time : DateTime -> Time- Visibility: public export
date : TyRE Date Date regex pattern: DD/MM/YYYY (24.03.1999)
Visibility: exporttime : TyRE Time Time regex pattern:
HH:mm (22:53)
HH:mm:ss (22:53:34)
Visibility: exportiso : TyRE DateTime ISO date
supported patterns:
YYYY-MM-DD (1999-03-24)
YYYY-MM-DDTHH:mm (1999-03-24T22:53)
YYYY-MM-DDTHH:mm:ss (1999-03-24T22:53:34)
YYYY-MM-DDTHH:mm:ss.sss (1999-03-24T22:53:34.011)
YYYY-MM-DDTHH:mm:ss.sss(+-)HH:mm (1999-03-24T22:53:34.011+01:00)
Visibility: export