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