Idris2Doc : IotaTime.Pattern.LocalTime

IotaTime.Pattern.LocalTime

(source)
Definitions
record TimeFieldsRep : Type
  Intermediate fields accumulated while parsing a local time.

  Totality: total
  Visibility: export
  Constructor: 
MkTimeFields : Integer -> Integer -> Integer -> Integer -> TimeFieldsRep

  Projections:
  
.parsedHour : TimeFieldsRep -> Integer
  
.parsedMinute : TimeFieldsRep -> Integer
  
.parsedNanosecond : TimeFieldsRep -> Integer
  
.parsedSecond : TimeFieldsRep -> Integer
TimeFields : Type
  Opaque intermediate state used by local-time patterns.

  Totality: total
  Visibility: public export
timeFields : Integer -> Integer -> Integer -> Integer -> TimeFields
  Seed omitted hour, minute, second, and nanosecond fields for `parseWith`.
  Parsed fields replace the corresponding seed values; final local-time
  validation still occurs after parsing.

  Totality: total
  Visibility: public export
phour : Nat -> Pattern TimeFields LocalTime
  A 24-hour field with the requested output width and up to two input digits.

  Totality: total
  Visibility: public export
pHH : Pattern TimeFields LocalTime
  A two-digit 24-hour field in the range 00 through 23.

  Totality: total
  Visibility: public export
phh : Pattern TimeFields LocalTime
  A two-digit 12-hour clock field in the range 01 through 12.

  Totality: total
  Visibility: public export
phhSpace : Pattern TimeFields LocalTime
  A space-padded two-character 12-hour clock field.

  Totality: total
  Visibility: public export
pminute : Nat -> Pattern TimeFields LocalTime
  A minute field with the requested output width and up to two input digits.

  Totality: total
  Visibility: public export
pmm : Pattern TimeFields LocalTime
  A two-digit minute field in the range 00 through 59.

  Totality: total
  Visibility: public export
psecond : Nat -> Pattern TimeFields LocalTime
  A second field with the requested output width and up to two input digits.

  Totality: total
  Visibility: public export
pss : Pattern TimeFields LocalTime
  A two-digit second field in the range 00 through 59.

  Totality: total
  Visibility: public export
isValidFractionWidth : Nat -> Bool
  Whether a fractional-second width is representable at nanosecond precision.

  Totality: total
  Visibility: public export
pfrac : (width : Nat) -> {auto 0 _ : So (isValidFractionWidth width)} -> Pattern TimeFields LocalTime
  A fixed-width fractional-second field with one through nine digits.
  
  The erased proof rejects unsupported widths at compile time.

  Totality: total
  Visibility: public export
pPeriod : (String, String) -> Pattern TimeFields LocalTime
  A 12-hour period field using the supplied AM and PM labels.

  Totality: total
  Visibility: public export
pp : Pattern TimeFields LocalTime
  The single-letter `A` or `P` period field.

  Totality: total
  Visibility: public export
ppp : Pattern TimeFields LocalTime
  The English `AM` or `PM` period field.

  Totality: total
  Visibility: public export
ppp' : Locale -> Pattern TimeFields LocalTime
  A period field using a locale's AM and PM labels.

  Totality: total
  Visibility: public export
pt : Pattern TimeFields LocalTime
  The short `HH:mm` local-time pattern.

  Totality: total
  Visibility: public export
pT : Pattern TimeFields LocalTime
  The long `HH:mm:ss` local-time pattern.

  Totality: total
  Visibility: public export
pr : Pattern TimeFields LocalTime
  The round-trip `HH:mm:ss.fffffffff` local-time pattern.

  Totality: total
  Visibility: public export