[TYPES] non-constuctive proofs

[Thorsten Altenkirch]

> By the way, I  reveal the a= sqrt{2}  and b = log_2 9 trick on page
> 51 of my notes!

Thanks to both of you. However, we may have learned at School how to  
prove that sqrt{2} is irrational. Is there an easy proof that log_2 9  
is?

Cheers,
Thorsten

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.