git.iko.soy/Idris-dev
on master help sign in
Effects summary was updated according to the current `Eff` definition.
cdf947aDenis Buzdalov
docs/effects/summary.rst+23−23
compare with master
unifiedsplit
@@ -43,16 +43,16 @@ FILE\_IO
43 data OpenFile : Mode -> Type
43 data OpenFile : Mode -> Type
44
44
45 open : (fname : String)
45 open : (fname : String)
46− -> (m : Mode)
46+ -> (m : Mode)
47− -> Eff Bool [FILE_IO ()]
47+ -> Eff Bool [FILE_IO ()]
48− (\res => [FILE_IO (case res of
48+ (\res => [FILE_IO (case res of
49− True => OpenFile m
49+ True => OpenFile m
50− False => ())])
50+ False => ())])
51 close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
51 close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
52
52
53− readLine : Eff String [FILE_IO (OpenFile Read)]
53+ readLine : Eff String [FILE_IO (OpenFile Read)]
54 writeLine : String -> Eff () [FILE_IO (OpenFile Write)]
54 writeLine : String -> Eff () [FILE_IO (OpenFile Write)]
55− eof : Eff Bool [FILE_IO (OpenFile Read)]
55+ eof : Eff Bool [FILE_IO (OpenFile Read)]
56
56
57 Handler FileIO IO where { ... }
57 Handler FileIO IO where { ... }
58
58
@@ -69,9 +69,9 @@ RND
69
69
70 RND : EFFECT
70 RND : EFFECT
71
71
72− srand : Integer -> Eff m () [RND]
72+ srand : Integer -> Eff () [RND]
73− rndInt : Integer -> Integer -> Eff m Integer [RND]
73+ rndInt : Integer -> Integer -> Eff Integer [RND]
74− rndFin : (k : Nat) -> Eff m (Fin (S k)) [RND]
74+ rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]
75
75
76 Handler Random m where { ... }
76 Handler Random m where { ... }
77
77
@@ -86,7 +86,7 @@ SELECT
86
86
87 SELECT : EFFECT
87 SELECT : EFFECT
88
88
89− select : List a -> Eff m a [SELECT]
89+ select : List a -> Eff a [SELECT]
90
90
91 Handler Selection Maybe where { ... }
91 Handler Selection Maybe where { ... }
92 Handler Selection List where { ... }
92 Handler Selection List where { ... }
@@ -102,10 +102,10 @@ STATE
102
102
103 STATE : Type -> EFFECT
103 STATE : Type -> EFFECT
104
104
105− get : Eff m x [STATE x]
105+ get : Eff x [STATE x]
106− put : x -> Eff m () [STATE x]
106+ put : x -> Eff () [STATE x]
107− putM : y -> Eff m () [STATE x] [STATE y]
107+ putM : y -> Eff () [STATE x] [STATE y]
108− update : (x -> x) -> Eff m () [STATE x]
108+ update : (x -> x) -> Eff () [STATE x]
109
109
110 Handler State m where { ... }
110 Handler State m where { ... }
111
111
@@ -121,12 +121,12 @@ STDIO
121
121
122 STDIO : EFFECT
122 STDIO : EFFECT
123
123
124− putChar : Handler StdIO m => Char -> Eff m () [STDIO]
124+ putChar : Char -> Eff () [STDIO]
125− putStr : Handler StdIO m => String -> Eff m () [STDIO]
125+ putStr : String -> Eff () [STDIO]
126− putStrLn : Handler StdIO m => String -> Eff m () [STDIO]
126+ putStrLn : String -> Eff () [STDIO]
127
127
128− getStr : Handler StdIO m => Eff m String [STDIO]
128+ getStr : Eff String [STDIO]
129− getChar : Handler StdIO m => Eff m Char [STDIO]
129+ getChar : Eff Char [STDIO]
130
130
131 Handler StdIO IO where { ... }
131 Handler StdIO IO where { ... }
132 Handler StdIO (IOExcept a) where { ... }
132 Handler StdIO (IOExcept a) where { ... }
@@ -144,9 +144,9 @@ SYSTEM
144
144
145 SYSTEM : EFFECT
145 SYSTEM : EFFECT
146
146
147− getArgs : Handler System e => Eff e (List String) [SYSTEM]
147+ getArgs : Eff (List String) [SYSTEM]
148− time : Handler System e => Eff e Int [SYSTEM]
148+ time : Eff Int [SYSTEM]
149− getEnv : Handler System e => String -> Eff e (Maybe String) [SYSTEM]
149+ getEnv : String -> Eff (Maybe String) [SYSTEM]
150
150
151 Handler System IO where { ... }
151 Handler System IO where { ... }
152 Handler System (IOExcept a) where { ... }
152 Handler System (IOExcept a) where { ... }