package dolmen

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

The type of terms.

val tType : ?loc:L.t -> unit -> t
val prop : ?loc:L.t -> unit -> t
val ty_int : ?loc:L.t -> unit -> t
val wildcard : ?loc:L.t -> unit -> t
val true_ : ?loc:L.t -> unit -> t
val false_ : ?loc:L.t -> unit -> t

Standard pre-defined constants.

val quoted : ?loc:L.t -> string -> t

Create an attribute from a quoted string.

val const : ?loc:L.t -> I.t -> t

Create a new constant.

val int : ?loc:L.t -> string -> t

Create an integer constant from a string.

val apply : ?loc:L.t -> t -> t list -> t

Application of terms.

val colon : ?loc:L.t -> t -> t -> t

Juxtaposition of terms, usually used for annotating terms with types.

val arrow : ?loc:L.t -> t -> t -> t

Arow, i.e function type constructor, currifyed.

val eq : ?loc:L.t -> t -> t -> t

Make an equality between terms.

val neq : ?loc:L.t -> t list -> t

Make an disequality between terms.

val not_ : ?loc:L.t -> t -> t
val or_ : ?loc:L.t -> t list -> t
val and_ : ?loc:L.t -> t list -> t
val imply : ?loc:L.t -> t -> t -> t
val equiv : ?loc:L.t -> t -> t -> t

Usual propositional functions.

val ite : ?loc:L.t -> t -> t -> t -> t

Conditional construction.

val pi : ?loc:L.t -> t list -> t -> t

Dependant product, or polymorphic type quantification. Used to build polymorphic function types such as, Pi [a] (Arrow a a).

val letin : ?loc:L.t -> t list -> t -> t

Local term binding.

val forall : ?loc:L.t -> t list -> t -> t

Universal propositional quantification.

val exists : ?loc:L.t -> t list -> t -> t

Existencial propositional qantification.

val match_ : ?loc:L.t -> t -> (t * t) list -> t

Pattern matching. The first term is the term to match, and each tuple in the list is a match case, which is a pair of a pattern and a match branch.

val lambda : ?loc:L.t -> t list -> t -> t

Create a lambda.

val uminus : ?loc:L.t -> t -> t

Arithmetic unary minus.

val add : ?loc:L.t -> t -> t -> t

Arithmetic addition.

val sub : ?loc:L.t -> t -> t -> t

Arithmetic substraction.

val mult : ?loc:L.t -> t -> t -> t

Arithmetic multiplication.

val lt : ?loc:L.t -> t -> t -> t

Arithmetic "lesser than" comparison (strict).

val leq : ?loc:L.t -> t -> t -> t

Arithmetic "lesser or equal" comparison.

val gt : ?loc:L.t -> t -> t -> t

Arithmetic "greater than" comparison (strict).

val geq : ?loc:L.t -> t -> t -> t

Arithmetic "greater or equal" comparison.

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