Re: [isabelle] Status of "eval" method



On Wed, 17 Oct 2012, Lukas Bulwahn wrote:

Removing is not possible as the Flyspeck proof relies on this method. In my opinion, renaming is not a reasonable option either.

On 10/17/2012 09:36 AM, Peter Lammich wrote:

So I propose to either add proper documentation for this method, including a warning that it does not go through the inference kernel, perhaps even renaming it to something like "eval_sorry", or to remove it.

"eval_sorry" would indeed be a rather odd name, because it is based on a different oracle that is supposed to be correct relative to the implementation of the code generator.

In contrast, the oracle behind "sorry" merely pretends that "!!X. X" holds, so you will be really sorry if you rely on the result.


	Makarius





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