The Coq mailing list

[Francois Pottier <Francois.Pottier AT inria.fr>]

Dear Coq users,

I would like to announce the first release of dblib, a library that is
supposed to help work with de Bruijn's encoding of binding.

The library is fairly reusable, and I have used it so far in two large proofs
of type soundness. Reusability is obtained in part via type classes, in part
via tactics that happen to "just work" (hopefully). The user is requested to
write a certain amount of boilerplate code, which I think remains tolerable.

The README file is here:

  http://gallium.inria.fr/~fpottier/dblib/README

and the complete distribution is here:

  http://gallium.inria.fr/~fpottier/dblib/dblib.tar.gz

There is no formal documentation, but the library itself is heavily commented,
and there are four little demos that help get started.

Your feedback is welcome. Enjoy!

-- 
François Pottier
Francois.Pottier AT inria.fr
http://gallium.inria.fr/~fpottier/