Module type Indexing.CARDINAL

A new type-level set is created by an application of the functors Const, Gensym, and Sum below. Each functor application creates a fresh type name n. More precisely, each functor application returns a module whose signature is CARDINAL: it contains both a fresh abstract type n and a value n of type n cardinal that represents the cardinal of the newly-created set.