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.

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 ommitted 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 ε)

def Std.Do.IO.Bare.instWPMonad {ε : Type} : WPMonad (EIO ε) (PostShape.except ε PostShape.pure)

Equations

• Std.Do.IO.Bare.instWPMonad = { toLawfulMonad := ⋯, toWP := Std.Do.IO.Bare.instWP, wp_pure := ⋯, wp_bind := ⋯ }