package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct