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.Refs.

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.

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