module type Term = Ast_tptp.Term
type
The type of terms.
type
The type of identifiers
type
The type of locations attached to terms.
val eq_t : t
val neq_t : t
val not_t : t
val or_t : t
val and_t : t
val xor_t : t
val nor_t : t
val nand_t : t
val equiv_t : t
val implies_t : t
val implied_t : t
val data_t : t
Predefined symbols in tptp. Symbols as standalone terms are necessary
for parsing tptp's THF. is reverse implication, and
is used in tptp's annotations.
val colon : ?loc:location ->
t -> t -> t
Juxtaposition of terms, usually used for annotating terms with their type.
val var : ?loc:location -> id -> t
Make a variable (in tptp, variable are syntaxically different from constants).
val const : ?loc:location -> id -> t
Make a constant.
val distinct : ?loc:location -> id -> t
Make a constant whose name possibly contain special characters
(All 'distinct' constants name are enclosed in quotes).
val int : ?loc:location -> string -> t
val rat : ?loc:location -> string -> t
val real : ?loc:location -> string -> t
Constants that are syntaxically recognised as numbers.
val apply : ?loc:location ->
t -> t list -> t
Application.
val ite : ?loc:location ->
t -> t -> t -> t
Conditional, of the form ite condition then_branch els_branch.
val union : ?loc:location ->
t -> t -> t
Union of types.
val product : ?loc:location ->
t -> t -> t
Product of types, used for function types with more than one argument.
val arrow : ?loc:location ->
t -> t -> t
Function type constructor.
val subtype : ?loc:location ->
t -> t -> t
Comparison of type (used in tptp's THF).
val pi : ?loc:location ->
t list -> t -> t
Dependant type constructor, used for polymorphic function types.
val letin : ?loc:location ->
t list -> t -> t
Local binding for terms.
val forall : ?loc:location ->
t list -> t -> t
Universal propositional quantification.
val exists : ?loc:location ->
t list -> t -> t
Existencial porpositional quantification.
val lambda : ?loc:location ->
t list -> t -> t
Function construction.
val choice : ?loc:location ->
t list -> t -> t
Indefinite description, also called choice operator.
val description : ?loc:location ->
t list -> t -> t
Definite description.
val sequent : ?loc:location ->
t list -> t list -> t
Sequents as terms, used as sequents hyps goals.