Re: [isabelle] value no longer pretty-prints numbers of type nat



Whether this is a bug or a feature, I would not dare to say. I can confirm that in Isabelle2013, you get pretty numerals for nat, but in Isabelle2013-RC-1, you don't get them by default. One could argue that the Suc representation is more faithful to the representation of nat, but for other types like int and rat, they are printed as pretty numerals.

If you import HOL/Library/Code_Target_Nat, then you get pretty numerals for nat, too. But of course, they are then implemented as target-language integers (rather than a datatype with constructors 0 and Suc).

Best,
Andreas

On 03/10/13 23:34, Christoph LANGE wrote:
Hi all,

with Isabelle 2013-1-RC1,

value "1::nat"

yields

"Suc 0"
   :: "nat"

instead of "1", which, I think, it did yield in Isabelle 2013.

Is this a bug, or is there a new configuration option I need to enable?

Cheers,

Christoph





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.