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 <ebe...@in.tum.de> wrote: >> >> the proper printing of "nat" values as numerals instead of successor >> notation.
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
