Re: [isabelle] Isabelle2014-RC0: Computations with rational numbers



Hi Jose,

thanks for reporting and investigating this.  I'll take a look after it.

Cheers,
	Florian

On 16.07.2014 14:44, Jose Divasón wrote:
> 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
> 

-- 

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.