[isabelle-dev] The coming release of Isabelle2017
eberlm at in.tum.de
Wed Jul 5 22:51:54 CEST 2017
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
On 2017-07-05 21:45, Lawrence Paulson wrote:
> What’s the idea here?
>> 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...
More information about the isabelle-dev