module Arith : sig ... endmodule Arrays : sig ... endmodule Base : sig ... endmodule Bitv : sig ... endmodule Core : sig ... endmodule Def : sig ... endDefinitions
module Float : sig ... endmodule Intf : sig ... endExternal Typechecker interface
module Logic : sig ... endmodule Misc : sig ... endMisc
module Strings : sig ... endmodule Tff : sig ... endTypechecking of standard terms This module provides functions to typecheck terms from the untyped syntax tree defined in the standard implementation.
module Tff_intf : sig ... endExternal Typechecker interface for TFF
module Thf : sig ... endTypechecking of standard terms This module provides functions to typecheck terms from the untyped syntax tree defined in the standard implementation.
module Thf_intf : sig ... endExternal Typechecker interface for THF