dolmen 0.7 · OCaml Package

type t

The type of terms.

val eq_t : ?loc:L.t -> unit -> t

val neq_t : ?loc:L.t -> unit -> t

val not_t : ?loc:L.t -> unit -> t

val or_t : ?loc:L.t -> unit -> t

val and_t : ?loc:L.t -> unit -> t

val xor_t : ?loc:L.t -> unit -> t

val nor_t : ?loc:L.t -> unit -> t

val nand_t : ?loc:L.t -> unit -> t

val equiv_t : ?loc:L.t -> unit -> t

val implies_t : ?loc:L.t -> unit -> t

val implied_t : ?loc:L.t -> unit -> t

val pi_t : ?loc:L.t -> unit -> t

val sigma_t : ?loc:L.t -> unit -> t

val data_t : ?loc:L.t -> unit -> t

Predefined symbols in tptp. Symbols as standalone terms are necessary for parsing tptp's THF. implied_t is reverse implication, and data_t is used in tptp's annotations. pi_t and sigma_t are the encoding of forall and exists quantifiers as constant in higher-order logic.

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

Juxtaposition of terms, usually used for annotating terms with their type.

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

Make a variable (in tptp, variable are syntaxically different from constants).

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

Make a constant.

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

Make a constant whose name possibly contain special characters (All 'distinct' constants name are enclosed in quotes).

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

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

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

Constants that are syntaxically recognised as numbers.

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

Application.

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

Conditional, of the form ite condition then_branch els_branch.

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

Union of types.

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

Product of types, used for function types with more than one argument.

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

Function type constructor.

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

Comparison of type (used in tptp's THF).

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

Dependant type constructor, used for polymorphic function types.

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

Local binding for terms.

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

Universal propositional quantification.

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

Existencial porpositional quantification.

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

Function construction.

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

Indefinite description, also called choice operator.

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

Definite description.

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

Sequents as terms, used as sequents hyps goals.

package dolmen