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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
