package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
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.