Idris2Doc : System.Time

System.Time

(source)
Reexports
import public Data.Fin
import public Data.Nat
Definitions
UntypedTime : Type
  Totality: total
  Visibility: public export
interface TimeValue : Type -> Type
  Parameters: a
Methods:
  
.millis : UntypedTime -> a
  
.seconds : UntypedTime -> a
  
.minutes : UntypedTime -> a
  
.hours : UntypedTime -> a
  
.days : UntypedTime -> a
  
.asMillis : a -> UntypedTime
  
.asSeconds : a -> UntypedTime
  
.asMinutes : a -> UntypedTime
  
.asHours : a -> UntypedTime
  
.asDays : a -> UntypedTime
  
.millisComponent : a -> Fin 1000
  
.secondsComponent : a -> Fin 60
  
.minutesComponent : a -> Fin 60
  
.hoursComponent : a -> Fin 24
  
.daysComponent : a -> Nat

Implementations:
  
TimeValue Time
  
TimeValue FinDuration
.millis : TimeValue a => UntypedTime -> a
  Totality: total
  Visibility: export
.seconds : TimeValue a => UntypedTime -> a
  Totality: total
  Visibility: export
.minutes : TimeValue a => UntypedTime -> a
  Totality: total
  Visibility: export
.hours : TimeValue a => UntypedTime -> a
  Totality: total
  Visibility: export
.days : TimeValue a => UntypedTime -> a
  Totality: total
  Visibility: export
.asMillis : TimeValue a => a -> UntypedTime
  Totality: total
  Visibility: export
.asSeconds : TimeValue a => a -> UntypedTime
  Totality: total
  Visibility: export
.asMinutes : TimeValue a => a -> UntypedTime
  Totality: total
  Visibility: export
.asHours : TimeValue a => a -> UntypedTime
  Totality: total
  Visibility: export
.asDays : TimeValue a => a -> UntypedTime
  Totality: total
  Visibility: export
.millisComponent : TimeValue a => a -> Fin 1000
  Totality: total
  Visibility: export
.secondsComponent : TimeValue a => a -> Fin 60
  Totality: total
  Visibility: export
.minutesComponent : TimeValue a => a -> Fin 60
  Totality: total
  Visibility: export
.hoursComponent : TimeValue a => a -> Fin 24
  Totality: total
  Visibility: export
.daysComponent : TimeValue a => a -> Nat
  Totality: total
  Visibility: export
record Time : Type
  Totality: total
  Visibility: export
  Constructor: 
MkTime : UntypedTime -> Time

  Projection: 
.millis : Time -> UntypedTime

  Hints:
  
Eq Time
  
Ord Time
  
TimeValue Time
record FinDuration : Type
  Totality: total
  Visibility: export
  Constructor: 
MkFinDuration : UntypedTime -> FinDuration

  Projection: 
.millis : FinDuration -> UntypedTime

  Hints:
  
Eq FinDuration
  
Monoid FinDuration
  
Ord FinDuration
  
Semigroup FinDuration
  
TimeValue FinDuration
DefaultTimeValue : TimeValue FinDuration
  Totality: total
  Visibility: export
(*) : Nat -> FinDuration -> FinDuration
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 9
(/) : FinDuration -> (z : Nat) -> {auto 0 _ : NonZero z} -> FinDuration
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 9
negate : Neg ty => ty -> ty
  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

  Totality: total
  Visibility: public export
  Fixity Declaration: prefix operator, level 10
(-) : FinDuration -> FinDuration -> FinDuration
  Totality: total
  Visibility: export
  Fixity Declarations:
  infixl operator, level 8
prefix operator, level 10
negate : Neg ty => ty -> ty
  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

  Totality: total
  Visibility: public export
  Fixity Declaration: prefix operator, level 10
(-) : Time -> Time -> FinDuration
  Totality: total
  Visibility: export
  Fixity Declarations:
  infixl operator, level 8
prefix operator, level 10
(+) : Time -> FinDuration -> Time
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 8
DefaultFinDurationInterpolation : Interpolation FinDuration
  Totality: total
  Visibility: export
interface Timed : (Type -> Type) -> Type
  Parameters: m
Methods:
  
currentTime : m Time

Implementation: 
Timed IO
currentTime : Timed m => m Time
  Totality: total
  Visibility: public export
interface CanSleep : (Type -> Type) -> Type
  Parameters: m
Constraints: Timed m, Monad m
Methods:
  
sleepTill : Time -> m ()
  
sleepFor : FinDuration -> m ()

Implementation: 
CanSleep IO
sleepTill : CanSleep m => Time -> m ()
  Totality: total
  Visibility: public export
sleepFor : CanSleep m => FinDuration -> m ()
  Totality: total
  Visibility: public export