[isabelle-dev] The coming release of Isabelle2017

[Manuel Eberl]

On 2017-07-05 22:09, Manuel Eberl wrote:
> I still want to take care of two really tiny things: […] and the proper printing
> of "nat" values as numerals instead of successor notation.

This is now done as of adf3155c57e2. I should note that I was somewhat
imprecise, by ‘printing of "nat" values’ I was only referring to what
you get when you type "value" etc. Now you won't get a screen full of
"Suc" when you do "value (1000 :: nat)", although computing with large
"nat" values is still relatively slow, as it uses "Suc" internally.

I am no expert on code generation, but I would imagine getting rid of
that (e.g. in favour of binary arithmetic, as is done for "int") is
probably non-trivial. What do our code generatione experts say?

In any case, it's probably not very important; "value" without
Code_Target_Numeral is mostly used for small-scale testing and the
current solution works fine for that.

Manuel