Utils.Time

Definitions

data Month : Type

Totality: total
Visibility: public export
Constructors:

January : Month

February : Month

March : Month

April : Month

May : Month

June : Month

July : Month

August : Month

September : Month

October : Month

November : Month

December : Month

Hints:

DecEq Month

Eq Month

Generic Month [[], [], [], [], [], [], [], [], [], [], [], []]

Meta Month [[], [], [], [], [], [], [], [], [], [], [], []]

Ord Month

Show Month

next_month : Month -> Month

Visibility: export

prev_month : Month -> Month

Visibility: export

next_prev_month : (m : Month) -> next_month (prev_month m) = m

Visibility: public export

prev_next_month : (m : Month) -> prev_month (next_month m) = m

Visibility: public export

nat_to_month : Nat -> Maybe Month

Visibility: export

fin_to_month : Fin 12 -> Month

Visibility: export

month_to_nat : Month -> Nat

Visibility: export

month_num_of_dates : Integer -> Month -> Nat

Visibility: export

data FinNonZero : Fin n -> Type

Totality: total
Visibility: public export
Constructor: 

FSIsNonZero : FinNonZero (FS x)

record Date : Type

Totality: total
Visibility: public export
Constructor: 

MkDate : (year : Integer) -> (month : Month) -> (day : Fin (S (month_num_of_dates year month))) -> FinNonZero day -> Date

Projections:

.day : ({rec:0} : Date) -> Fin (S (month_num_of_dates (year {rec:0}) (month {rec:0})))

.day_non_zero : ({rec:0} : Date) -> FinNonZero (day {rec:0})

.month : Date -> Month

.year : Date -> Integer

Hints:

Eq Date

Ord Date

Show Date

.year : Date -> Integer

Visibility: public export

year : Date -> Integer

Visibility: public export

.month : Date -> Month

Visibility: public export

month : Date -> Month

Visibility: public export

.day : ({rec:0} : Date) -> Fin (S (month_num_of_dates (year {rec:0}) (month {rec:0})))

Visibility: public export

day : ({rec:0} : Date) -> Fin (S (month_num_of_dates (year {rec:0}) (month {rec:0})))

Visibility: public export

.day_non_zero : ({rec:0} : Date) -> FinNonZero (day {rec:0})

Visibility: public export

day_non_zero : ({rec:0} : Date) -> FinNonZero (day {rec:0})

Visibility: public export

epoch_date : Date

Visibility: export

days_between_dates : Date -> Date -> Integer

Visibility: export

record DateTime : Type

Totality: total
Visibility: public export
Constructor: 

MkDateTime : Date -> Fin 24 -> Fin 60 -> Fin 60 -> Fin 1000 -> Bool -> Nat -> Fin 60 -> DateTime

Projections:

.date : DateTime -> Date

.hour : DateTime -> Fin 24

.hour_offset : DateTime -> Nat

.minute : DateTime -> Fin 60

.minute_offset : DateTime -> Fin 60

.offset_plus_or_minus : DateTime -> Bool

.second : DateTime -> Fin 60

.subsecond : DateTime -> Fin 1000

Hint: 

Show DateTime

.date : DateTime -> Date

Visibility: public export

date : DateTime -> Date

Visibility: public export

.hour : DateTime -> Fin 24

Visibility: public export

hour : DateTime -> Fin 24

Visibility: public export

.minute : DateTime -> Fin 60

Visibility: public export

minute : DateTime -> Fin 60

Visibility: public export

.second : DateTime -> Fin 60

Visibility: public export

second : DateTime -> Fin 60

Visibility: public export

.subsecond : DateTime -> Fin 1000

Visibility: public export

subsecond : DateTime -> Fin 1000

Visibility: public export

.offset_plus_or_minus : DateTime -> Bool

Visibility: public export

offset_plus_or_minus : DateTime -> Bool

Visibility: public export

.hour_offset : DateTime -> Nat

Visibility: public export

hour_offset : DateTime -> Nat

Visibility: public export

.minute_offset : DateTime -> Fin 60

Visibility: public export

minute_offset : DateTime -> Fin 60

Visibility: public export

epoch_to_datetime : Integer -> DateTime

Visibility: export

millisecond_epoch_to_datetime : Integer -> DateTime

Visibility: export

gmt_datetime : DateTime -> DateTime

Visibility: export

datetime_to_epoch : DateTime -> Integer

Visibility: export

millisecond_datetime_to_epoch : DateTime -> Integer

Visibility: export

utc_time : Monad m => ParseT m DateTime

Visibility: export

generalized_time : Monad m => ParseT m DateTime

Visibility: export

parse_utc_time : String -> Either String DateTime

Visibility: export

parse_generalized_time : String -> Either String DateTime

Visibility: export