mathlib documentation

core / system.io_interface

inductive io.error  :
Type
Instances for io.error
  • io.error.has_sizeof_inst
inductive io.mode  :
Type
Instances for io.mode
  • io.mode.has_sizeof_inst
inductive io.process.stdio  :
Type
Instances for io.process.stdio
  • io.process.stdio.has_sizeof_inst
structure io.process.spawn_args  :
Type
Instances for io.process.spawn_args
  • io.process.spawn_args.has_sizeof_inst
@[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 of this typeclass
Instances of other typeclasses for monad_io
  • monad_io.has_sizeof_inst
@[class]
structure monad_io_terminal (m : Type → Type → Type) :
Type
Instances of this typeclass
Instances of other typeclasses for monad_io_terminal
  • monad_io_terminal.has_sizeof_inst
@[class]
structure monad_io_net_system (m : Type → Type → Type) [monad_io m] :
Type 1
Instances of this typeclass
Instances of other typeclasses for monad_io_net_system
  • monad_io_net_system.has_sizeof_inst
@[class]
structure monad_io_file_system (m : Type → Type → Type) [monad_io m] :
Type
Instances of this typeclass
Instances of other typeclasses for monad_io_file_system
  • monad_io_file_system.has_sizeof_inst
@[class]
meta structure monad_io_serial (m : Type → Type → Type) [monad_io m] :
Type
Instances of this typeclass
@[class]
structure monad_io_environment (m : Type → Type → Type) :
Type
Instances of this typeclass
Instances of other typeclasses for monad_io_environment
  • monad_io_environment.has_sizeof_inst
@[class]
structure monad_io_process (m : Type → Type → Type) [monad_io m] :
Type 1
Instances of this typeclass
Instances of other typeclasses for monad_io_process
  • monad_io_process.has_sizeof_inst
@[class]
structure monad_io_random (m : Type → Type → Type) :
Type
Instances of this typeclass
Instances of other typeclasses for monad_io_random
  • monad_io_random.has_sizeof_inst
@[protected, instance]
def monad_io_is_monad (m : Type → Type → Type) (e : Type) [monad_io m] :
monad (m e)
Equations
@[protected, instance]
def monad_io_is_monad_fail (m : Type → Type → Type) [monad_io m] :
Equations
@[protected, instance]
def monad_io_is_alternative (m : Type → Type → Type) [monad_io m] :
Equations