ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 03:34:13 +03:00
Code Issues Projects Releases Wiki Activity

Fixed comment of Effect type; ordering incorrect and vague.

Browse Source
This commit is contained in:
Craig McLaughlin 2015-10-09 11:43:52 +01:00
parent 6ee21c78fa
commit 7806ff594f
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libs/effects/Effects.idr
View File

@ -12,9 +12,9 @@ import Data.Vect
||| The Effect type describes effectful computations.
|||
||| This type is parameterised by:
||| + The input resource.
||| + The return type of the computation.
||| + The computation to run on the resource.
||| + The input resource.
||| + The computation to run on the resource given the return value.
Effect : Type
Effect = (x : Type) -> Type -> (x -> Type) -> Type