mathlib documentation

core.system.io_interface

inductive io.error  :
Type

inductive io.mode  :
Type

inductive io.process.stdio  :
Type

structure io.process.spawn_args  :
Type

@[class]
structure monad_io  :
(Type → Type → Type)Type 1
  • monad : Π (e : Type), monad (m e)
  • catch : Π (e₁ e₂ α : Type), m e₁ α(e₁ → m e₂ α)m e₂ α
  • fail : Π (e α : Type), e → m e α
  • iterate : Π (e α : Type), α → (α → m e (option α))m e α
  • handle : Type

Instances
@[class]
structure monad_io_terminal  :
(Type → Type → Type) → Type

Instances
@[class]
structure monad_io_net_system (m : Type → Type → Type) [monad_io m] :
Type 1

Instances
@[class]
structure monad_io_file_system (m : Type → Type → Type) [monad_io m] :
Type

Instances
@[class]
meta structure monad_io_serial (m : Type → Type → Type) [monad_io m] :
Type

Instances
@[class]
structure monad_io_environment  :
(Type → Type → Type) → Type

Instances
@[class]
structure monad_io_process (m : Type → Type → Type) [monad_io m] :
Type 1

Instances
@[class]
structure monad_io_random  :
(Type → Type → Type) → Type

Instances
@[instance]
def monad_io_is_monad (m : Type → Type → Type) (e : Type) [monad_io m] :
monad (m e)

Equations
@[instance]
def monad_io_is_monad_fail (m : Type → Type → Type) [monad_io m] :

Equations
@[instance]
def monad_io_is_alternative (m : Type → Type → Type) [monad_io m] :

Equations