Logic_monad.BackState
val return : 'a -> ( 'a, 's, 's, 'e ) t
val set : 'o -> ( unit, 'i, 'o, 'e ) t
val get : ( 's, 's, 's, 'e ) t
val modify : ( 'i -> 'o ) -> ( unit, 'i, 'o, 'e ) t
interleave 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 ) t
val lift : 'a NonLogical.t -> ( 'a, 's, 's, 'e ) t
val repr :
( 'a, 'e ) reified ->
( 'a, ( 'a, 'e ) reified_, 'e ) list_view_ NonLogical.t