package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/coq-core.clib/Option/index.html
Module Option
Source
Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library.
Actually, some operations have the same name as List
ones: they actually are similar considering 'a option
as a type of lists with at most one element.
has_some x
is true
if x
is of the form Some y
and false
otherwise.
Negation of has_some
equal f x y
lifts the equality predicate f
to option types. That is, if both x
and y
are None
then it returns true
, if they are both Some _
then f
is called. Otherwise it returns false
.
Same as equal
, but with comparison.
Lift a hash to option types.
get x
returns y
where x
is Some y
.
make x
returns Some x
.
bind x f
is f y
if x
is Some y
and None
otherwise
filter f x
is x
if x
Some y
and f y
is true, None
otherwise
init b x
returns Some x
if b
is true
and None
otherwise.
flatten x
is Some y
if x
is Some (Some y)
and None
otherwise.
append x y
is the first element of the concatenation of x
and y
seen as lists. In other words, append (Some a) y
is Some a
, append None (Some b)
is Some b
, and append None None
is None
.
"Iterators"
iter f x
executes f y
if x
equals Some y
. It does nothing otherwise.
iter2 f x y
executes f z w
if x
equals Some z
and y
equals Some w
. It does nothing if both x
and y
are None
.
map f x
is None
if x
is None
and Some (f y)
if x
is Some y
.
fold_left f a x
is f a y
if x
is Some y
, and a
otherwise.
fold_left2 f a x y
is f z w
if x
is Some z
and y
is Some w
. It is a
if both x
and y
are None
.
fold_right f x a
is f y a
if x
is Some y
, and a
otherwise.
fold_left_map f a x
is a, f y
if x
is Some y
, and a
otherwise.
Same as fold_left_map
on the right
cata f e x
is e
if x
is None
and f a
if x
is Some a
More Specific Operations
default a x
is y
if x
is Some y
and a
otherwise.