The Module System

A theory of dictionaries

In order to illustrate Coq's module system, we present a theory of dictionnaries implemented as functors, which is a certified version of an example by L. Paulson in Standard ML (In ML for the working Programmer, Cambridge University Press, 1996, pp 280-284)


The complete source

Exercises

Exercise 12.1 page 339 Lexicographic ordering on lists (with functors)
Going home
Pierre Castéran