Module type `Dolmen_tptp.Term`Source

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.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/dolmen.tptp/Dolmen_tptp/module-type-Term/index.html

Module type `Dolmen_tptp.Term`Source

package dolmen

Install

Dune Dependency

Authors

Maintainers

Sources

doc/dolmen.tptp/Dolmen_tptp/module-type-Term/index.html

Module type Dolmen_tptp.TermSource

Module type `Dolmen_tptp.Term`Source