Module Libzipperposition.SimplMSource

Simplification Monad

This monad is used to combine simplifications in a way that allows to know if at least one simplification was performed, or not.

Sourcetype +'a t = 'a * [ `Same | `New ]
Sourceval return_same : 'a -> 'a t
Sourceval return_new : 'a -> 'a t
Sourceval return : 'a -> 'a t

Alias to return_same

Sourceval return_opt : old:'a -> 'a option -> 'a t

return_opt ~old t returns return_new u if t=Some u, else returns same old.

Sourceval get : 'a t -> 'a
Sourceval is_new : _ t -> bool
Sourceval is_same : _ t -> bool
Sourceval (>>=) : 'a t -> ('a -> 'b t) -> 'b t

Monadic bind

Sourceval map : ('a -> 'b) -> 'a t -> 'b t
Sourceval app_list : ('a -> 'a t) list -> 'a -> 'a t
Sourceval map_l : ('a -> 'b t) -> 'a list -> 'b list t
Sourceval fold_l : ('a -> 'b -> 'a t) -> 'a -> 'b list -> 'a t
Sourcemodule Infix : sig ... end