The Coq mailing list

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

Dear Coq users,

I would like to announce the availability of a little library that helps
define a simple do/while loop in Coq. (More generally, any tail-recursive
function can be expressed in this style.) The library does not rely on any
axioms. At the level of the extracted OCaml code, it has zero overhead.

A more detailed description is online:

  https://github.com/fpottier/loop

At least part of this functionality is already offered by Coq's Function and
Program commands. Maybe all of it, I am not sure. Apologies for re-inventing
the wheel. Anyway, your comments and suggestions are welcome.

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