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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
