Module Dolmen_intf.TySource

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

Sourcemodule type Tff = sig ... end

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

Sourcemodule type Thf = sig ... end
Sourcemodule type Ae_Base = sig ... end

Signature required by types for typing ae

Sourcemodule type Ae_Arith = sig ... end

Signature required by types for typing ae's arithmetic

Sourcemodule type Ae_Array = sig ... end

Signature required by types for typing ae arrays

Sourcemodule type Ae_Bitv = sig ... end

Signature required by types for typing ae's bitvectors

Sourcemodule type Tptp_Base = sig ... end

Signature required by types for typing tptp

Sourcemodule type Tptp_Arith = sig ... end

Signature required by types for typing tptp

Sourcemodule type Smtlib_Base = sig ... end

Signature required by types for typing smtlib core theory

Sourcemodule type Smtlib_Int = sig ... end

Signature required by types for typing smtlib integer arithmetic

Sourcemodule type Smtlib_Real = sig ... end

Signature required by types for typing smtlib real arithmetic

Sourcemodule type Smtlib_Real_Int = sig ... end

Signature required by types for typing smtlib real_int arithmetic.

Sourcemodule type Smtlib_Array = sig ... end

Signature required by types for typing smtlib arrays

Sourcemodule type Smtlib_Bitv = sig ... end

Signature required by types for typing smtlib bitvectors

Sourcemodule type Smtlib_Float = sig ... end

Signature required by types for typing smtlib bitvectors

Sourcemodule type Smtlib_String = sig ... end
Sourcemodule type Zf_Base = sig ... end

Signature required by types for typing tptp

Sourcemodule type Zf_Arith = sig ... end

Signature required by types for typing tptp