[isabelle-dev] The coming release of Isabelle2017

[Manuel Eberl]

Nothing fancy, just a couple of code_post rules to rewrite successor
notation into numeral notation after evaluation and before printing. I
don't know if there's a better way to do that, but I think we discussed
this on the mailing list a while ago and came to the conclusion that
code_post is indeed the way to go.

Of course, I am always open to better solutions, perhaps avoiding the
successor notation entirely, but I don't know the code generator well
enough to say if this is possible (or where the successor stuff comes
from in the first place)

In any case, I would argue that even those code_post rules to rewrite
successor notation to numerals is a lot better than what we have at the
moment.

Manuel


On 2017-07-05 21:45, Lawrence Paulson wrote:
> What’s the idea here?
> Larry
>
>> On 5 Jul 2017, at 21:09, Manuel Eberl <eberlm at in.tum.de> wrote:
>>
>> the proper printing of "nat" values as numerals instead of successor notation.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170705/4785b45b/attachment-0002.html>