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.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

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