# [isabelle] Problem with pretty printing rationals

```Dear all,

```
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.)
```

consts show_rat
```
axioms show_rat_def[code]: "show_rat (Fract a b) = (if b = 1 then show_int a else show_int a @ ''/'' @ show_int b)"
```
```
Now, the code-generator is working. However, I do not like to add axioms to my theory, so is there a better way around? 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?
```
Thanks a lot,
```
René
```
```

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