Idris2Doc : Control.App

Control.App

(>>=) : SafeBindll' => Appea -> (a -> Appeb) -> Appeb

Fixity Declaration: infixl operator, level 1
dataApp : {defaultMayThrow_ : Path} -> ListError -> Type -> Type
  A type supports throwing and catching exceptions. See `interface Exception err e` for details.
@ l An implicit Path states whether the program's execution path is linear or might throw
exceptions. The default value is `MayThrow` which represents that the program might throw.
@ es A list of exception types that can be thrown. Constrained interfaces can be defined by
parameterising with a list of errors `es`.

Totality: total
Constructor: 
MkApp : (1 _ : ((1 _ : %World) -> AppRes (execTylet))) -> Appet
dataApp1 : {defaultOne_ : Usage} -> ListError -> Type -> Type
Totality: total
Constructor: 
MkApp1 : (1 _ : ((1 _ : %World) -> App1Resut)) -> App1et
dataAppHasIO : Type
  When type is present in app "errors" list, app is allowed to perform I/O.

Totality: total
Cont1Type : Usage -> Type -> Usage -> ListError -> Type -> Type
Error : Type
  `Error` is a type synonym for `Type`, specify for exception handling.

Exception : Error -> ListError -> Type
  An alias for `HasErr`.

dataFileEx : Type
Totality: total
Constructors:
GenericFileEx : Int -> FileEx
FileReadError : FileEx
FileWriteError : FileEx
FileNotFound : FileEx
PermissionDenied : FileEx
FileExists : FileEx
Has : List (a -> Type) -> a -> Type
dataHasErr : Error -> ListError -> Type
Totality: total
Constructors:
Here : HasErre (e::es)
There : HasErrees -> HasErre (e'::es)
dataIOError : Type
Totality: total
Constructors:
GenericErr : String -> IOError
FileErr : FileEx -> IOError
Init : ListError
dataPath : Type
  States whether the program's execution path is linear or might throw exceptions so that we can know
whether it is safe to reference linear resources.

Totality: total
Constructors:
MayThrow : Path
NoThrow : Path
interfacePrimIO : ListError -> Type
Parameters: e
Methods:
primIO : IOa -> Appea
primIO1 : (1 _ : IOa) -> App1ea
fork : (PrimIOe' => Appe' ()) -> Appe ()

Implementation: 
HasErrAppHasIOe => PrimIOe
dataSafeBind : Path -> Path -> Type
Totality: total
Constructors:
SafeSame : SafeBindll
SafeToThrow : SafeBindNoThrowMayThrow
dataState : a -> Type -> ListError -> Type
Totality: total
Constructor: 
MkState : IOReft -> Statetagte
dataUsage : Type
Totality: total
Constructors:
One : Usage
Any : Usage
app : (1 _ : Appea) -> App1ea
app1 : (1 _ : App1ea) -> Appea
bindApp1 : (1 _ : App1ea) -> (1 _ : Cont1Typeuau'eb) -> App1eb
bindL : Appea -> (1 _ : (a -> Appeb)) -> Appeb
catch : HasErrerres => Appesa -> (err -> Appesa) -> Appesa
fork : PrimIOe => (PrimIOe' => Appe' ()) -> Appe ()
get : (0 tag : _) -> Statetagte => Appet
handle : App (err::e) a -> (a -> Appeb) -> (err -> Appeb) -> Appeb
lift : Appea -> App (err::e) a
mapState : Statetagte -> Statetagt (eff::e)
modify : (0 tag : _) -> Statetagte => (t -> t) -> Appe ()
new : t -> (Statetagte => Appea) -> Appea
new1 : t -> (1 _ : (Statetagte => App1ea)) -> App1ea
noThrow : AppInita -> AppInita
primIO : PrimIOe => IOa -> Appea
primIO1 : PrimIOe => (1 _ : IOa) -> App1ea
put : (0 tag : _) -> Statetagte => t -> Appe ()
run : AppInita -> IOa
  The only way provided by `Control.App` to run an App.
@ Init A concrete list of errors.

throw : HasErrerres => err -> Appesa