package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
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.