dolmen_type

A typechecker for automated deduction languages
IN THIS PACKAGE
Module Dolmen_type
module Arith : sig ... end
module Arrays : sig ... end
module Base : sig ... end
module Bitv : sig ... end
module Core : sig ... end
module Def : sig ... end

Definitions

module Float : sig ... end
module Intf : sig ... end

External Typechecker interface

module Logic : sig ... end
module Misc : sig ... end

Misc

module Strings : sig ... end
module Tff : sig ... end

Typechecking of standard terms This module provides functions to typecheck terms from the untyped syntax tree defined in the standard implementation.

module Tff_intf : sig ... end

External Typechecker interface for TFF

module Thf : sig ... end

Typechecking of standard terms This module provides functions to typecheck terms from the untyped syntax tree defined in the standard implementation.

module Thf_intf : sig ... end

External Typechecker interface for THF