*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Problem with pretty printing rationals*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Thu, 12 Nov 2009 11:27:26 +0100*In-reply-to*: <4AFA891F.8090006@in.tum.de>*References*: <14D9AEB2-EF02-4185-97B5-FF100956CF0A@uibk.ac.at> <4AFA854B.4020107@in.tum.de> <4AFA891F.8090006@in.tum.de>

The function should be called "normalize :: rat => int * int" andshouldalso take care of the sign: the denominator should be positive. Since gcd is there already, it is easy to define directly. Any takers?

Cheers, René

Tobias Alexander Krauss wrote:Hi René,I just encountered the following problem. When writing a pretty printer for rational numbers the standard function I would like to write is: show_rat (Fract a b) = (if b = 1 then show_int a else show_int a @ ''/'' @ show_int b)" However, since Fract is a only a code_datatype and not a datatype,Isabelle refused this function definition. (And it must refuse,sinceFract 1 2 = Fract 2 4, but show_rat .. = 1/2 != 2/4 = show_rat .. Hence, show_rat is not a function.)Right. This cannot work.Are there for example functions like "get_numerator" and "get_denominator" which return unique results independent of whether using (Fract 1 2) or (Fract 2 4) which I overlooked in Rational.thy?There aren't, but it seems that they should be there, socontributionsare welcome (probably a function that returns (int * int) is best).Itcan be defined using THE. Alex

**References**:**[isabelle] Problem with pretty printing rationals***From:*René Thiemann

**Re: [isabelle] Problem with pretty printing rationals***From:*Alexander Krauss

**Re: [isabelle] Problem with pretty printing rationals***From:*Tobias Nipkow

- Previous by Date: [isabelle] SBMF 2010 - First Call for Papers
- Next by Date: [isabelle] Question about Code Generator
- Previous by Thread: Re: [isabelle] Problem with pretty printing rationals
- Next by Thread: [isabelle] Does anyone know how to get rid of => marker in PG4.0?
- Cl-isabelle-users November 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list