mathlib3 documentation

core / system.io_interface

inductive io.error  :
Instances for io.error
  • io.error.has_sizeof_inst
inductive io.mode  :
Instances for io.mode
  • io.mode.has_sizeof_inst
inductive io.process.stdio  :
Instances for io.process.stdio
  • io.process.stdio.has_sizeof_inst
structure io.process.spawn_args  :
Instances for io.process.spawn_args
  • io.process.spawn_args.has_sizeof_inst
@[class]
structure monad_io (m : Type Type 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) :
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] :
Instances of this typeclass
Instances of other typeclasses for monad_io_net_system
  • monad_io_net_system.has_sizeof_inst
@[class]
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] :
Instances of this typeclass
@[class]
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] :
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) :
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]
Equations
@[protected, instance]
Equations