- piped : io.process.stdio
- inherit : io.process.stdio
- null : io.process.stdio
- cmd : string
- args : list string
- stdin : io.process.stdio
- stdout : io.process.stdio
- stderr : io.process.stdio
- cwd : option string
- env : list (string × option string)
@[class]
Instances
@[class]
- socket : Type
- listen : string → ℕ → m io.error (monad_io_net_system.socket m)
- accept : monad_io_net_system.socket m → m io.error (monad_io_net_system.socket m)
- connect : string → m io.error (monad_io_net_system.socket m)
- recv : monad_io_net_system.socket m → ℕ → m io.error char_buffer
- send : monad_io_net_system.socket m → char_buffer → m io.error unit
- close : monad_io_net_system.socket m → m io.error unit
Instances
@[class]
- mk_file_handle : string → io.mode → bool → m io.error (monad_io.handle m)
- is_eof : monad_io.handle m → m io.error bool
- flush : monad_io.handle m → m io.error unit
- close : monad_io.handle m → m io.error unit
- read : monad_io.handle m → ℕ → m io.error char_buffer
- write : monad_io.handle m → char_buffer → m io.error unit
- get_line : monad_io.handle m → m io.error char_buffer
- stdin : m io.error (monad_io.handle m)
- stdout : m io.error (monad_io.handle m)
- stderr : m io.error (monad_io.handle m)
- file_exists : string → m io.error bool
- dir_exists : string → m io.error bool
- remove : string → m io.error unit
- rename : string → string → m io.error unit
- mkdir : string → bool → m io.error bool
- rmdir : string → m io.error bool
Instances
@[class]
- serialize : monad_io.handle m → expr → m io.error unit
- deserialize : monad_io.handle m → m io.error expr
Instances
@[class]
- child : Type
- stdin : monad_io_process.child m → monad_io.handle m
- stdout : monad_io_process.child m → monad_io.handle m
- stderr : monad_io_process.child m → monad_io.handle m
- spawn : io.process.spawn_args → m io.error (monad_io_process.child m)
- wait : monad_io_process.child m → m io.error ℕ
- sleep : ℕ → m io.error unit
Instances
@[class]
Instances
@[instance]
Equations
- monad_io_is_monad m e = monad_io.monad e
@[instance]
Equations
- monad_io_is_monad_fail m = {fail := λ (α : Type) (s : string), monad_io.fail io.error α (io.error.other s)}
@[instance]
Equations
- monad_io_is_alternative m = {to_applicative := {to_functor := {map := λ (_x _x_1 : Type) (x : _x → _x_1) (y : m io.error _x), has_pure.pure x <*> y, map_const := λ (α β : Type), (λ (x : β → α) (y : m io.error β), has_pure.pure x <*> y) ∘ function.const β}, to_has_pure := applicative.to_has_pure monad.to_applicative, to_has_seq := applicative.to_has_seq monad.to_applicative, to_has_seq_left := {seq_left := λ (α β : Type) (a : m io.error α) (b : m io.error β), (λ (_x _x_1 : Type) (x : _x → _x_1) (y : m io.error _x), has_pure.pure x <*> y) α (β → α) (function.const β) a <*> b}, to_has_seq_right := {seq_right := λ (α β : Type) (a : m io.error α) (b : m io.error β), (λ (_x _x_1 : Type) (x : _x → _x_1) (y : m io.error _x), has_pure.pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := λ (α : Type) (a b : m io.error α), monad_io.catch io.error io.error α a (λ (_x : io.error), b)}, failure := λ (α : Type), monad_io.fail io.error α (io.error.other "failure")}