# Barebones `WP` instance for `IO` #

This module defines a `WP` instance for `IO` without any synthetic model of the `IO.RealWorld` whatsoever. This is useful for reasoning about `IO` programs when the precise result of a side-effect is irrelevant; for example it can be used to reason about random number generation. It is however inadequate for reasoning about, e.g., `IO.Ref`s.

source
noncomputable def Std.Do.IO.Bare.instWP {ε : Type} :
WP (EIO ε) (PostShape.except ε PostShape.pure)

This is pretty much the instance for `EStateM` specialized to `σ = IO.RealWorld`. However, `IO.RealWorld` is omitted in the `PredShape`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Std.Do.IO.Bare.instLawfulMonad {ε : Type} :
LawfulMonad (EIO ε)