Idris2Doc : Data.Time.Date

Data.Time.Date

(source)
Definitions
record Year : Type
  Totality: total
  Visibility: public export
  Constructor: 
Y : (year : Integer) -> {auto 0 _ : FromTo 0 9999 year} -> Year

  Projections:
  
0 .valid : ({rec:0} : Year) -> FromTo 0 9999 (year {rec:0})
  
.year : Year -> Integer

  Hints:
  
Eq Year
  
Interpolation Year
  
Ord Year
  
Show Year
.year : Year -> Integer
  Totality: total
  Visibility: public export
year : Year -> Integer
  Totality: total
  Visibility: public export
0 .valid : ({rec:0} : Year) -> FromTo 0 9999 (year {rec:0})
  Totality: total
  Visibility: public export
0 valid : ({rec:0} : Year) -> FromTo 0 9999 (year {rec:0})
  Totality: total
  Visibility: public export
data Month : Type
  Totality: total
  Visibility: public export
  Constructors:
  
JAN : Month
  
FEB : Month
  
MAR : Month
  
APR : Month
  
MAY : Month
  
JUN : Month
  
JUL : Month
  
AUG : Month
  
SEP : Month
  
OCT : Month
  
NOV : Month
  
DEC : Month

  Hints:
  
Eq Month
  
Eq (Day m)
  
Interpolation Month
  
Interpolation (Day m)
  
Ord Month
  
Ord (Day m)
  
Show Month
  
Show (Day m)
DaysInMonth : Month -> Integer
  Totality: total
  Visibility: public export
intToMonth : Integer -> Maybe Month
  Totality: total
  Visibility: public export
record Day : Month -> Type
  Totality: total
  Visibility: public export
  Constructor: 
D : (day : Integer) -> {auto 0 _ : FromTo 1 (DaysInMonth m) day} -> Day m

  Projections:
  
.day : Day m -> Integer
  
0 .valid : ({rec:0} : Day m) -> FromTo 1 (DaysInMonth m) (day {rec:0})

  Hints:
  
Eq (Day m)
  
Interpolation (Day m)
  
Ord (Day m)
  
Show (Day m)
.day : Day m -> Integer
  Totality: total
  Visibility: public export
day : Day m -> Integer
  Totality: total
  Visibility: public export
0 .valid : ({rec:0} : Day m) -> FromTo 1 (DaysInMonth m) (day {rec:0})
  Totality: total
  Visibility: public export
0 valid : ({rec:0} : Day m) -> FromTo 1 (DaysInMonth m) (day {rec:0})
  Totality: total
  Visibility: public export
refineDay : Integer -> Maybe (Day m)
  Totality: total
  Visibility: public export
fromInteger : (n : Integer) -> {auto 0 _ : IsJust (refineDay (cast n))} -> Day m
  Totality: total
  Visibility: public export
record Date : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDate : Year -> (month : Month) -> Day month -> Date

  Projections:
  
.day : ({rec:0} : Date) -> Day (month {rec:0})
  
.month : Date -> Month
  
.year : Date -> Year

  Hints:
  
Eq Date
  
Interpolation Date
  
Ord Date
  
Show Date
.year : Date -> Year
  Totality: total
  Visibility: public export
year : Date -> Year
  Totality: total
  Visibility: public export
.month : Date -> Month
  Totality: total
  Visibility: public export
month : Date -> Month
  Totality: total
  Visibility: public export
.day : ({rec:0} : Date) -> Day (month {rec:0})
  Totality: total
  Visibility: public export
day : ({rec:0} : Date) -> Day (month {rec:0})
  Totality: total
  Visibility: public export