dolmen

A parser library for automated deduction
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen.intf
Module Dolmen_intf . Ty

Signature for Typecheked types

module type Tff = sig ... end

Signature required by types for typing first-order polymorphic terms.

module type Thf = sig ... end
module type Ae_Base = sig ... end

Signature required by types for typing ae

module type Ae_Arith = sig ... end

Signature required by types for typing ae's arithmetic

module type Ae_Array = sig ... end

Signature required by types for typing ae arrays

module type Ae_Bitv = sig ... end

Signature required by types for typing ae's bitvectors

module type Tptp_Base = sig ... end

Signature required by types for typing tptp

module type Tptp_Arith = sig ... end

Signature required by types for typing tptp

module type Smtlib_Base = sig ... end

Signature required by types for typing smtlib core theory

module type Smtlib_Int = sig ... end

Signature required by types for typing smtlib integer arithmetic

module type Smtlib_Real = sig ... end

Signature required by types for typing smtlib real arithmetic

module type Smtlib_Real_Int = sig ... end

Signature required by types for typing smtlib real_int arithmetic.

module type Smtlib_Array = sig ... end

Signature required by types for typing smtlib arrays

module type Smtlib_Bitv = sig ... end

Signature required by types for typing smtlib bitvectors

module type Smtlib_Float = sig ... end

Signature required by types for typing smtlib bitvectors

module type Smtlib_String = sig ... end
module type Zf_Base = sig ... end

Signature required by types for typing tptp

module type Zf_Arith = sig ... end

Signature required by types for typing tptp