Module Dolmen_intf.Ty

Interfaces for Types This module defines Interfaces that implementation of types must respect in order to be used to instantiate functors.

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