Re: [isabelle] Non terminating function proven terminating

Thanks for all the comments: I now understand a bit more the philosophy
behind Isabelle. Given that extraction remains safe (I guess that the simps
equations are the one used to generate the code?), I suppose that this is
just a matter of taste.


On 22 October 2011 13:58, Makarius <makarius at> wrote:
> You quote this like something that is well-known in the constructive
> community.  Can you point to some mailing list threads discussing it, or
> similar?

I don't know if it's really well-known: I was just giving credits to the one
that discovered it. In the meantime Andreas Abel told me that it was actually
older than Pierre's remark:

« No this trick is old, and documented in Barthe et al, MSCS 2004, page 3,
point 3b. »

On 22 October 2011 23:53, Alexander Krauss <krauss at> wrote:
> You seem to be using a specific notion of "well-defined", probably coming
> from constructive type theory.

Guilty as charged! Now that I put back my classical glasses, I can understand
that "\lambda (). ()" can also be seen as a well defined solution (it
works + every
other solution has to be extensionally equal).

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.