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



See now http://isabelle.in.tum.de/reports/Isabelle/rev/083dfad2727c.

	Florian

On 19.07.2014 17:51, Florian Haftmann wrote:
> 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.