Module type `Dolmen_zf.Term`Source

Sourcetype t

The type of terms.

Sourcetype id

The type of identifiers

Sourcetype location

The type of locations attached to terms.

Sourceval tType : ?loc:location -> unit -> t

Sourceval prop : ?loc:location -> unit -> t

Sourceval ty_int : ?loc:location -> unit -> t

Sourceval wildcard : ?loc:location -> unit -> t

Sourceval true_ : ?loc:location -> unit -> t

Sourceval false_ : ?loc:location -> unit -> t

Standard pre-defined constants.

Sourceval quoted : ?loc:location -> string -> t

Create an attribute from a quoted string.

Sourceval const : ?loc:location -> id -> t

Create a new constant.

Sourceval int : ?loc:location -> string -> t

Create an integer constant from a string.

Sourceval apply : ?loc:location -> t -> t list -> t

Application of terms.

Sourceval colon : ?loc:location -> t -> t -> t

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

Sourceval arrow : ?loc:location -> t -> t -> t

Arow, i.e function type constructor, currifyed.

Sourceval eq : ?loc:location -> t -> t -> t

Make an equality between terms.

Sourceval neq : ?loc:location -> t list -> t

Make an disequality between terms.

Sourceval not_ : ?loc:location -> t -> t

Sourceval or_ : ?loc:location -> t list -> t

Sourceval and_ : ?loc:location -> t list -> t

Sourceval imply : ?loc:location -> t -> t -> t

Sourceval equiv : ?loc:location -> t -> t -> t

Usual propositional functions.

Sourceval ite : ?loc:location -> t -> t -> t -> t

Conditional construction.

Sourceval pi : ?loc:location -> t list -> t -> t

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

Sourceval letin : ?loc:location -> t list -> t -> t

Local term binding.

Sourceval forall : ?loc:location -> t list -> t -> t

Universal propositional quantification.

Sourceval exists : ?loc:location -> t list -> t -> t

Existencial propositional qantification.

Sourceval match_ : ?loc:location -> 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.

Sourceval lambda : ?loc:location -> t list -> t -> t

Create a lambda.

Sourceval uminus : ?loc:location -> t -> t

Arithmetic unary minus.

Sourceval add : ?loc:location -> t -> t -> t

Arithmetic addition.

Sourceval sub : ?loc:location -> t -> t -> t

Arithmetic substraction.

Sourceval mult : ?loc:location -> t -> t -> t

Arithmetic multiplication.

Sourceval lt : ?loc:location -> t -> t -> t

Arithmetic "lesser than" comparison (strict).

Sourceval leq : ?loc:location -> t -> t -> t

Arithmetic "lesser or equal" comparison.

Sourceval gt : ?loc:location -> t -> t -> t

Arithmetic "greater than" comparison (strict).

Sourceval geq : ?loc:location -> t -> t -> t

Arithmetic "greater or equal" comparison.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/dolmen.zf/Dolmen_zf/module-type-Term/index.html

Module type `Dolmen_zf.Term`Source

package dolmen

Install

Dune Dependency

Authors

Maintainers

Sources

doc/dolmen.zf/Dolmen_zf/module-type-Term/index.html

Module type Dolmen_zf.TermSource

Module type `Dolmen_zf.Term`Source