[isabelle-dev] Evaluation of floor and ceiling

[Lukas Bulwahn]

Hi all,


Jasmin has pointed out that the evaluation of floor and ceiling showed 
surprising behaviour and I looked into the topic:

If we are interested to enable evaluation of terms such as "floor (5 / 6 
:: rat)" or "ceiling (1 / 2 :: real)", this will require different code 
equations for the different types -- hence the definition of floor and 
ceiling would have to be moved into the archimedian type class, and then 
one could provide actually different instantiations for the evaluation.
This seems like a non-trivial refactoring.


Is anyone interested to use evaluation for such terms which might 
motivate to do this refactoring?


Lukas