Module Smyth.Nondet
Construction
val none : 'a t
The empty nondeterministic computation (i.e., one with no possible outcomes); useful for cutting off a nondeterministic computation.
val from_list : 'a list -> 'a t
Treats each entry in the list as a possible nondeterministic outcome.
Collection
val to_list : 'a t -> 'a list
Collects all possible nondeterministic outputs.
Core functions
Generic library functions
Specific library functions
val union : 'a t list -> 'a t
Takes a list of nondeterministic computations and (conceptually) nondeterministically chooses just one of the computations to perform; the "sum" operation.
val one_of_each : 'a t list -> 'a list t
Takes a list of nondeterministic computations and (conceptually) chooses one computation from each to perform; the "product" operation.
val is_empty : 'a t -> bool
Checks if a nondeterministic computation is empty (no possible outcomes).
val filter : ('a -> bool) -> 'a t -> 'a t
Filters all possible nondeterministic outcomes with a predicate.
val collapse_option : 'a option t -> 'a t
Filters all possible nondeterministic outcomes to include only those that are
Some
thing.
Lifting
Syntax
module Syntax : sig ... end