= 1024" x-on:close-sidebar="sidebar=window.innerWidth >= 1024 && true">
package dolmen
-
dolmen
-
dolmen.intf
-
-
dolmen.line
-
dolmen.smtlib2
-
dolmen.std
-
-
dolmen.tptp
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Type definitions
Common definitions
type 'a tag = 'a Tag.t
Type definitions
type builtin =
< ty : ty
; ty_var : ty_var
; ty_cst : ty_cst
; term : term
; term_var : term_var
; term_cst : term_cst >
Builtin.t
Extensible variant type for builtin operations.
The type of identifiers. 'ty
is the type for representing the type of the id.
and pattern = term
patterns are simply terms
and term = {
term_ty : ty;
term_descr : term_descr;
mutable term_hash : hash;
mutable term_tags : Tag.map;
}
Term, which wrap term descriptions.
and formula = term
Alias for signature compatibility (with Dolmen_loop.Pipes.Make for instance).
Exceptions
exception Already_aliased of ty_cst
exception Type_already_defined of ty_cst
exception Record_type_expected of ty_cst
Native Tags
module Tags : sig ... end
Printing
module Print : sig ... end
Substitutions
module Subst : sig ... end
Module to handle substitutions
Identifiers
module Id : sig ... end
Types
module Ty : sig ... end
Terms
module Term : sig ... end
Signature required by terms for typing first-order polymorphic terms.