Email Gateway (Aug 19 2022 at 12:04): Email Gateway (Aug 19 2022 at 12:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Aug 19 2022 at 12:07):From: Christoph LANGE <math.semantic.web@gmail.com>
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
Email Gateway (Aug 19 2022 at 12:18):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Nov 21 2024 at 12:39 UTC