Idris2Doc : IotaTime.Tzdb.Tzif

IotaTime.Tzdb.Tzif

(source)
Reexports
import public Data.Bits
import public IotaTime.TimeZone.Core
Definitions
data TzifVersion : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Version1 : TzifVersion
  
Version2 : TzifVersion
  
Version3 : TzifVersion
  
Version4 : TzifVersion

  Hint: 
Eq TzifVersion
data TzifError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
UnexpectedEnd : TzifError
  
InvalidMagic : TzifError
  
UnsupportedVersion : Bits8 -> TzifError
  
InvalidSecondHeader : TzifError
  
MissingTransitionType : TzifError
  
InvalidTransitionTypeIndex : Integer -> TzifError
  
InvalidAbbreviationIndex : Integer -> TzifError
  
UnterminatedAbbreviation : Integer -> TzifError
  
InvalidUtcOffset : Integer -> TzifError
  
InvalidFooter : TzifError
  
TrailingData : TzifError
record TzifData : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTzifData : TzifVersion -> TransitionInfo -> List (Instant, TransitionInfo) -> Maybe String -> TzifData

  Projections:
  
.initialTransition : TzifData -> TransitionInfo
  
.posixFooter : TzifData -> Maybe String
  
.transitions : TzifData -> List (Instant, TransitionInfo)
  
.version : TzifData -> TzifVersion
.version : TzifData -> TzifVersion
  Totality: total
  Visibility: public export
version : TzifData -> TzifVersion
  Totality: total
  Visibility: public export
.initialTransition : TzifData -> TransitionInfo
  Totality: total
  Visibility: public export
initialTransition : TzifData -> TransitionInfo
  Totality: total
  Visibility: public export
.transitions : TzifData -> List (Instant, TransitionInfo)
  Totality: total
  Visibility: public export
transitions : TzifData -> List (Instant, TransitionInfo)
  Totality: total
  Visibility: public export
.posixFooter : TzifData -> Maybe String
  Totality: total
  Visibility: public export
posixFooter : TzifData -> Maybe String
  Totality: total
  Visibility: public export
parseTzif : List Bits8 -> Either TzifError TzifData
  Decode a complete TZif file. POSIX future rules are retained as text and
  are not silently approximated by the final explicit transition.

  Totality: total
  Visibility: public export