package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8

doc/lambdapi.lplib/Lplib/Option/index.html

Module Lplib.OptionSource

include module type of struct include Option end

Options

Sourceval none : 'a option

none is None.

Sourceval some : 'a -> 'a option

some v is Some v.

Sourceval value : 'a option -> default:'a -> 'a

value o ~default is v if o is Some v and default otherwise.

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

bind o f is f v if o is Some v and None if o is None.

Sourceval join : 'a option option -> 'a option

join oo is Some v if oo is Some (Some v) and None otherwise.

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

map f o is None if o is None and Some (f v) if o is Some v.

Sourceval product : 'a option -> 'b option -> ('a * 'b) option

product o0 o1 is Some (v0, v1) if o0 is Some v0 and o1 is Some v1 and None otherwise.

  • since 5.5
Sourceval iter : ('a -> unit) -> 'a option -> unit

iter f o is f v if o is Some v and () otherwise.

Sourceval blend : ('a -> 'a -> 'a) -> 'a option -> 'a option -> 'a option

blend f o1 o2 is o1 if o2 is None, o2 if o1 is None, and Some (f v1 v2) if o1 is Some v1 and o2 is Some v2.

  • since 5.5
Sourceval for_all : ('a -> bool) -> 'a option -> bool

for_all p behaves like List.for_all p on a list of zero or one element:

  • for_all p None is true,
  • for_all p (Some v) is p v.
  • since 5.5
Sourceval exists : ('a -> bool) -> 'a option -> bool

exists p behaves like List.exists p on a list of zero or one element:

  • exists p None is false,
  • exists p (Some v) is p v.
  • since 5.5

Predicates and comparisons

Sourceval is_none : 'a option -> bool

is_none o is true if and only if o is None.

Sourceval is_some : 'a option -> bool

is_some o is true if and only if o is Some o.

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

equal eq o0 o1 is true if and only if o0 and o1 are both None or if they are Some v0 and Some v1 and eq v0 v1 is true.

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

compare cmp o0 o1 is a total order on options using cmp to compare values wrapped by Some _. None is smaller than Some _ values.

Converting

Sourceval to_result : none:'e -> 'a option -> ('a, 'e) result

to_result ~none o is Ok v if o is Some v and Error none otherwise.

Sourceval to_list : 'a option -> 'a list

to_list o is [] if o is None and [v] if o is Some v.

Sourceval to_seq : 'a option -> 'a Seq.t

to_seq o is o as a sequence. None is the empty sequence and Some v is the singleton sequence containing v.

Syntax

Sourcemodule Syntax = Option.Syntax

Binding operators. See manual section 12.23 for details.

Sourcetype 'a t = 'a option
Sourceval is_None : 'a t -> bool
Sourceval get : 'a -> 'a option -> 'a
Sourceval map_default : ('a -> 'b) -> 'b -> 'a option -> 'b
Sourceval fold : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a
Sourceval cmp : 'a Base.cmp -> 'a option Base.cmp
Sourceval eq : 'a Base.eq -> 'a option Base.eq
Sourceval pp : 'a Base.pp -> 'a option Base.pp
Sourcemodule Monad : sig ... end
Sourcemodule Applicative : sig ... end