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 (m : 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 (m : 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 (m : 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 (m : 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