Idris2Doc : IotaTime.Calendar.Component

IotaTime.Calendar.Component

(source)
Reexports
import public Data.So
Definitions
record Year : Type
  A calendar year with an unbounded signed integer value.

  Totality: total
  Visibility: export
  Constructor: 
MkYear : Integer -> Year

  Projection: 
.integerValue : Year -> Integer

  Hints:
  
Eq Year
  
Neg Year
  
Num Year
  
Ord Year
  
Show Year
fromInteger : Integer -> Year
  Construct a year from any integer.

  Totality: total
  Visibility: public export
yearValue : Year -> Integer
  Return the signed integer represented by a year.

  Totality: total
  Visibility: public export
yearFromInteger : Integer -> Year
  Totality: total
  Visibility: export
record DayOfMonth : Type
  A day number constrained to the inclusive range 1 through 31.

  Totality: total
  Visibility: export
  Constructor: 
MkDayOfMonth : Integer -> DayOfMonth

  Projection: 
.integerValue : DayOfMonth -> Integer

  Hints:
  
Eq DayOfMonth
  
Ord DayOfMonth
  
Show DayOfMonth
isValidDayOfMonth : Integer -> Bool
  Whether an integer is in the representable day-of-month range.

  Totality: total
  Visibility: public export
fromInteger : (value : Integer) -> {auto 0 _ : So (isValidDayOfMonth value)} -> DayOfMonth
  Construct a day of month when its range proof is available statically.

  Totality: total
  Visibility: public export
dayOfMonthValue : DayOfMonth -> Integer
  Return the integer day number.

  Totality: total
  Visibility: public export
dayOfMonthFromInteger : Integer -> DayOfMonth
  Totality: total
  Visibility: export
data DayOfMonthError : Type
  A runtime day-of-month value outside the inclusive range 1 through 31.

  Totality: total
  Visibility: public export
  Constructor: 
DayOfMonthOutOfRange : Integer -> DayOfMonthError
refineDayOfMonth : Integer -> Either DayOfMonthError DayOfMonth
  Refine an untrusted integer into a day of month or return a typed range error.

  Totality: total
  Visibility: public export
record WeekNumber : Type
  An unbounded signed week number used by calendar week calculations.

  Totality: total
  Visibility: export
  Constructor: 
MkWeekNumber : Integer -> WeekNumber

  Projection: 
.integerValue : WeekNumber -> Integer

  Hints:
  
Eq WeekNumber
  
Neg WeekNumber
  
Num WeekNumber
  
Ord WeekNumber
  
Show WeekNumber
fromInteger : Integer -> WeekNumber
  Construct a week number from any integer.

  Totality: total
  Visibility: public export
weekNumberValue : WeekNumber -> Integer
  Return the signed integer represented by a week number.

  Totality: total
  Visibility: public export