Structures · Lean core

Std.Do.WPMonad

A monad with weakest preconditions (WP) that is also a monad morphism, preserving pure and bind. In practice, mvcgen is not useful for reasoning about programs in a monad that is without a WPMonad instance. The specification lemmas for Pure.pure and Bind.bind, as well as those for operators like Functor.map, require that their monad have a WPMonad instance.

Defined in

Std.Do.WP.Monad

Shape

2 explicit arguments · adds wp_pure, wp_bind