package linksem
-
linksem_zarith
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
error is a type used to represent potentially failing computations. Success * marks a successful completion of a computation, whilst Fail err marks a failure, * with err as the reason.
val return : 'a -> 'a errorreturn is the monadic lifting function for error, representing a successful * computation.
val with_success : 'a error -> 'b -> ('a -> 'b) -> 'bval fail : string -> 'a errorfail err represents a failing computation, with error message err.
as_maybe e drops an error value into a maybe value, throwing away * error information.
val as_maybe : 'a error -> 'a optionval of_maybe : string -> 'a option -> 'a errorval repeatM'' : Nat_big_num.num -> 'a error -> 'a list error -> 'a list errorrepeatM count action fails if action is a failing computation, or * successfully produces a list count elements long, where each element is * the value successfully returned by action.
val repeatM : Nat_big_num.num -> 'a error -> 'a list errorval repeatM' :
Nat_big_num.num ->
'b ->
('b -> ('a * 'b) error) ->
('a list * 'b) errorrepeatM' count seed action is a variant of repeatM that acts like repeatM * apart from any successful result returns a tuple whose second component is seed * and whose first component is the same as would be returned by repeatM.
mapM f xs maps f across xs, failing if f fails on any element of xs.
foldM f e xs performs a monadic right fold of f across xs using e * as the base case. Fails if any application of f fails.
val string_of_error : 'a Show.show_class -> 'a error -> stringstring_of_error err produces a string representation of err.
val instance_Show_Show_Error_error_dict :
'a Show.show_class ->
'a error Show.show_class