Module Syntax

module Poly : sig ... end

This module provides functionalities for representing polynomials.

module Rule : sig ... end

This module provides functionality to represent rewriting rules.

module Symb : sig ... end

This module exports a module type NAME, which is an abstract interface for names, and one module IndexedName of type NAME.

module Term : sig ... end

This module provides functionality for the notion of terms.

module Ty : sig ... end

Implementation of simple types. This module exports the functor MakeSType, a Sort module of type Symb.NAME, and a concrete simple types implementation in SType.