Logic_monad.BackStateval return : 'a -> ( 'a, 's, 's, 'e ) tval set : 'o -> ( unit, 'i, 'o, 'e ) tval get : ( 's, 's, 's, 'e ) tval modify : ( 'i -> 'o ) -> ( unit, 'i, 'o, 'e ) tinterleave src dst m adapts the exceptional content of the monad according to the functions src and dst. To ensure a meaningful result, those functions must form a retraction, i.e. dst (src e1) = e1 for all e1. This is typically the case when the type 'e1 is unit.
val zero : 'e -> ( 'a, 'i, 'o, 'e ) tval lift : 'a NonLogical.t -> ( 'a, 's, 's, 'e ) tval repr :
( 'a, 'e ) reified ->
( 'a, ( 'a, 'e ) reified_, 'e ) list_view_ NonLogical.t