package dolmen

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

Module type Dolmen_tptp.TermSource

Sourcetype t

The type of terms.

Sourcetype id

The type of identifiers

Sourcetype location

The type of locations attached to terms.

Sourceval eq_t : ?loc:location -> unit -> t
Sourceval neq_t : ?loc:location -> unit -> t
Sourceval not_t : ?loc:location -> unit -> t
Sourceval or_t : ?loc:location -> unit -> t
Sourceval and_t : ?loc:location -> unit -> t
Sourceval xor_t : ?loc:location -> unit -> t
Sourceval nor_t : ?loc:location -> unit -> t
Sourceval nand_t : ?loc:location -> unit -> t
Sourceval equiv_t : ?loc:location -> unit -> t
Sourceval implies_t : ?loc:location -> unit -> t
Sourceval implied_t : ?loc:location -> unit -> t
Sourceval data_t : ?loc:location -> 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.

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

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

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

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

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

Make a constant.

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

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

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

Constants that are syntaxically recognised as numbers.

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

Application.

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

Conditional, of the form ite condition then_branch els_branch.

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

Union of types.

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

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

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

Function type constructor.

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

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

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

Dependant type constructor, used for polymorphic function types.

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

Local binding for terms.

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

Universal propositional quantification.

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

Existencial porpositional quantification.

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

Function construction.

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

Indefinite description, also called choice operator.

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

Definite description.

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

Sequents as terms, used as sequents hyps goals.