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 sketis.net> 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
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 in.tum.de> 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