package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

doc/coq-core.clib/Option/index.html

Module OptionSource

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.

Sourceexception IsNone
Sourceval has_some : 'a option -> bool

has_some x is true if x is of the form Some y and false otherwise.

Sourceval is_empty : 'a option -> bool

Negation of has_some

Sourceval equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool

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.

Sourceval compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int

Same as equal, but with comparison.

Sourceval hash : ('a -> int) -> 'a option -> int

Lift a hash to option types.

Sourceval get : 'a option -> 'a

get x returns y where x is Some y.

  • raises IsNone

    if x equals None.

Sourceval make : 'a -> 'a option

make x returns Some x.

Sourceval bind : 'a option -> ('a -> 'b option) -> 'b option

bind x f is f y if x is Some y and None otherwise

Sourceval filter : ('a -> bool) -> 'a option -> 'a option

filter f x is x if x Some y and f y is true, None otherwise

Sourceval init : bool -> 'a -> 'a option

init b x returns Some x if b is true and None otherwise.

Sourceval flatten : 'a option option -> 'a option

flatten x is Some y if x is Some (Some y) and None otherwise.

Sourceval append : 'a option -> 'a option -> 'a option

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"
Sourceval iter : ('a -> unit) -> 'a option -> unit

iter f x executes f y if x equals Some y. It does nothing otherwise.

Sourceexception Heterogeneous
Sourceval iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit

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.

Sourceval map : ('a -> 'b) -> 'a option -> 'b option

map f x is None if x is None and Some (f y) if x is Some y.

Sourceval fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b

fold_left f a x is f a y if x is Some y, and a otherwise.

Sourceval fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a

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.

Sourceval fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b

fold_right f x a is f y a if x is Some y, and a otherwise.

Sourceval fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option

fold_left_map f a x is a, f y if x is Some y, and a otherwise.

Sourceval fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b option -> 'a -> 'c option * 'a

Same as fold_left_map on the right

Sourceval cata : ('a -> 'b) -> 'b -> 'a option -> 'b

cata f e x is e if x is None and f a if x is Some a

More Specific Operations
Sourceval default : 'a -> 'a option -> 'a

default a x is y if x is Some y and a otherwise.

Smart operations
Sourcemodule Smart : sig ... end
Operations with Lists
Sourcemodule List : sig ... end