Parameter Make.T

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.