# Re: [isabelle] Problem with pretty printing rationals

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, since
``Fract 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, so contributions
are welcome (probably a function that returns (int * int) is best). It
can be defined using THE.
Alex

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*