Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2014-RC0: Computations with rational n...


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 12:29 UTC