dolmen

A parser library for automated deduction
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen.ae
Parameter #2 Dolmen_ae . Make . I
type t

The type of identifiers

type namespace

The type for namespaces.

val var : namespace

Used for type variables.

val term : namespace

Usual namespace, used for terms and propositions.

val sort : namespace

Usual namespace, used for types.

val decl : namespace

Names used to refer to tptp phrases. These are used in declarations and include statement.

val track : namespace

Namespace used to tag and identify sub-terms occuring in files.

val mk : namespace -> string -> t

Make an identifier

val tracked : track:t -> namespace -> string -> t

Make an identifier with an additional name.