package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

exception IsNone
val has_some : 'a option -> bool

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

val is_empty : 'a option -> bool

Negation of has_some

val 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.

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

Same as equal, but with comparison.

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

Lift a hash to option types.

val get : 'a option -> 'a

get x returns y where x is Some y.

  • raises IsNone

    if x equals None.

val make : 'a -> 'a option

make x returns Some x.

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

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

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

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

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

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

val flatten : 'a option option -> 'a option

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

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

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

exception Heterogeneous
val 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.

val 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.

val 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.

val 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.

val 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.

val 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.

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

Same as fold_left_map on the right

val 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
val default : 'a -> 'a option -> 'a

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

val lift : ('a -> 'b) -> 'a option -> 'b option

lift is the same as map.

val lift_right : ('a -> 'b -> 'c) -> 'a -> 'b option -> 'c option

lift_right f a x is Some (f a y) if x is Some y, and None otherwise.

val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option

lift_left f x a is Some (f y a) if x is Some y, and None otherwise.

val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option

lift2 f x y is Some (f z w) if x equals Some z and y equals Some w. It is None otherwise.

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