<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p><font size="+1">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.<br>
      </font></p>
    <p><font size="+1">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)</font></p>
    <p><font size="+1">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.<br>
      </font></p>
    <p><font size="+1">Manuel<br>
      </font></p>
    <br>
    <div class="moz-cite-prefix">On 2017-07-05 21:45, Lawrence Paulson
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:3EA4ACE8-CD5E-4537-868E-D0B701DA92DB@cam.ac.uk">
      <pre wrap="">What’s the idea here?
Larry

</pre>
      <blockquote type="cite">
        <pre wrap="">On 5 Jul 2017, at 21:09, Manuel Eberl <a class="moz-txt-link-rfc2396E" href="mailto:eberlm@in.tum.de"><eberlm@in.tum.de></a> wrote:

the proper printing of "nat" values as numerals instead of successor notation.
</pre>
      </blockquote>
      <pre wrap="">
</pre>
    </blockquote>
    <br>
  </body>
</html>