Email Gateway (Aug 19 2022 at 14:54): Email Gateway (Aug 19 2022 at 14:54):From: Jose Divasón <jose.divasonm@unirioja.es>
Dear all,
I would like to report a minor issue involving rational numbers. Attached
and also at the end of this message you can find an example.
If one runs such file using Isabelle2013-2, for each value its output shows
something like:
"-1 / 2" :: "rat"
However, in Isabelle2014-RC0 the outputs are different:
"Frct (int_of_integer (- 1), 2)" :: "rat"
Is this the expected behaviour?
I think that everything comes from the following version (the elimination
of neg_numeral): http://isabelle.in.tum.de/repos/isabelle/rev/03ff4d1e6784
I have tried to get the former output looking at the print_codeproc and
print_codesetup, but I don't see where the problem is.
Thanks,
Jose
theory Foo
imports
Rat
"~~/src/HOL/Library/Code_Target_Numeral"
begin
value "int_of_integer (- 1)"
value "-1::rat"
value "(-1/2)::rat"
value "(-2/4)::rat"
value "-(1/2)::rat"
value "(1/-2)::rat"
value "Fract (-1) (2)"
value "Fract 1 (-2)"
end
Foo.thy
Email Gateway (Aug 19 2022 at 14:57):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jose,
thanks for reporting and investigating this. I'll take a look after it.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 14:58):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now http://isabelle.in.tum.de/reports/Isabelle/rev/083dfad2727c.
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC