Idris2Doc : Data.Time.Time

Data.Time.Time

(source)
Reexports
import public Data.Nat
import public Data.Refined
import public Data.Time.Date
import public Data.Refined.Integer
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 : LocalDate -> LocalTime -> LocalDateTime

  Projections:
  
.date : LocalDateTime -> LocalDate
  
.time : LocalDateTime -> LocalTime

  Hints:
  
Eq LocalDateTime
  
Interpolation LocalDateTime
  
Show LocalDateTime
.date : LocalDateTime -> LocalDate
  Totality: total
  Visibility: public export
date : LocalDateTime -> LocalDate
  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 : LocalDate -> OffsetTime -> OffsetDateTime

  Projections:
  
.date : OffsetDateTime -> LocalDate
  
.time : OffsetDateTime -> OffsetTime

  Hints:
  
Eq OffsetDateTime
  
Interpolation OffsetDateTime
  
Show OffsetDateTime
.date : OffsetDateTime -> LocalDate
  Totality: total
  Visibility: public export
date : OffsetDateTime -> LocalDate
  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:
  
ATLocalDate : LocalDate -> AnyTime
  
ATLocalTime : LocalTime -> AnyTime
  
ATLocalDateTime : LocalDateTime -> AnyTime
  
ATOffsetDateTime : OffsetDateTime -> AnyTime

  Hints:
  
Eq AnyTime
  
Interpolation AnyTime
  
Show AnyTime
getDate : AnyTime -> Maybe LocalDate
  Totality: total
  Visibility: export
extraCheckDate : AnyTime -> Either LocalDate AnyTime
  Totality: total
  Visibility: export