The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Mon, 1 Aug 2011 17:01:30 +0200
AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
>
> Ok, you didn't understood my response; my script proved what you wished
> (at least on my version of Coq), so that your formalization may be
> wrong (the eternal problem of "how can I be sure I am in the theory I
> want?"), but what you intended to prove was provable, so it doesn't seem
> meaningless.

Well, in this case, given that it was adapted from a working O'Caml
implementation and that there's an informal termination proof in the
book it was published with, I think the formalization is probably OK.

Whether or not what I'm trying to prove is actually worth proving is
*another* matter, but it's really just for learning experience at this
point.