Idris2Doc : IotaTime.Offset

IotaTime.Offset

(source)
Reexports
import public Data.So
Definitions
record OffsetRep : Type
  A signed whole-second displacement from UTC, bounded to plus or minus
  eighteen hours.

  Totality: total
  Visibility: export
  Constructor: 
MkOffset : Integer -> OffsetRep

  Projection: 
.storedSeconds : OffsetRep -> Integer

  Hints:
  
Eq OffsetRep
  
Ord OffsetRep
  
Show OffsetRep
Offset : Type
  Totality: total
  Visibility: public export
isValidOffsetSeconds : Integer -> Bool
  Totality: total
  Visibility: public export
isValidOffsetMinutes : Integer -> Bool
  Totality: total
  Visibility: public export
isValidOffsetHours : Integer -> Bool
  Totality: total
  Visibility: public export
fromSeconds : (value : Integer) -> {auto 0 _ : So (isValidOffsetSeconds value)} -> Offset
  Totality: total
  Visibility: public export
fromMinutes : (value : Integer) -> {auto 0 _ : So (isValidOffsetMinutes value)} -> Offset
  Totality: total
  Visibility: public export
fromHours : (value : Integer) -> {auto 0 _ : So (isValidOffsetHours value)} -> Offset
  Totality: total
  Visibility: public export
data OffsetError : Type
  Totality: total
  Visibility: public export
  Constructor: 
OffsetOutOfRange : Integer -> OffsetError
refineOffsetSeconds : Integer -> Either OffsetError Offset
  Totality: total
  Visibility: public export
totalOffsetSeconds : Offset -> Integer
  Internal exact-value observation used by sibling implementation modules.
  Public callers should normally use `hours`, `minutes`, and `seconds`.

  Totality: total
  Visibility: export
hours : Offset -> Integer
  The signed whole-hour component of an offset.

  Totality: total
  Visibility: public export
minutes : Offset -> Integer
  The signed minute-within-hour component of an offset.

  Totality: total
  Visibility: public export
seconds : Offset -> Integer
  The signed second-within-minute component of an offset.

  Totality: total
  Visibility: public export
empty : Offset
  Totality: total
  Visibility: public export
addClamped : Offset -> Offset -> Offset
  Add two offsets, clamping the result to the supported bounds.

  Totality: total
  Visibility: public export
minusClamped : Offset -> Offset -> Offset
  Subtract the second offset, clamping the result to the supported bounds.

  Totality: total
  Visibility: public export
negateOffset : Offset -> Offset
  Reverse an offset's direction.

  Totality: total
  Visibility: public export