Documentation

The IO State object

Lean uses two channels for sending output to the user:

• A regular output channel, which consists of messages normally printed to stdout.
• A diagnostic output channel, which consists of debugging messages that are normally printed to stderr.

This module currently provides two different IOState types:

• A standard IO state that sends regular output to stdout and diagnostic output to stderr.
• A buffered IO state type that stores output internally, and provides methods for getting output as strings.

To prevent users from accidentally using the wrong type of output, the IOState has an extra type-level parameter used to indicate the type of channel. Most Lean operations support both types of channels and either can be used. Operations specific to a particular channel can use this type parameter to ensure users do not call the function on the wrong type of channel. In addition, we provide a function stateTypeRepr to allow users to determine the type of channel.

Run a computation with an io state.

Lift an arbitray IOState to SomeIOState

This describes the type of the IOState.

Internal state used for bindings

Haskell type for lean_ios FFI parameters.

Haskell type for lean_ios* FFI parameters.

Function c2hs uses to pass SomeIOState values to Lean

Type synonym for c2hs to use specifically for functions that expected buffered IO state.

Function c2hs uses to pass BufferedIOState values to Lean