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



> 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?

It is both a bug and a feature, the same way as it is none of both.

To be clear in the beginning, both representations are logically sound.

For technical reasons, the reconstruction of Isabelle terms from ML
terms was hand-made for nat, and used numerals.  In Isabelle 2013-1-RC1,
this is not necessary any longer, and just the default reconstruction is
used, which obeys the set of constructors for a particular type.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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