Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Quick and dirty evaluation of reals

view this post on Zulip Email Gateway (Aug 11 2022 at 07:41):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

starting with an observation by Achim Brucker, I had a look at quick and
dirty evaluation of reals and realized a lot of issues and deficiencies
had accumulated over the years.

I tried to consolidate that finally in Isabelle rev. a21debbc7074 and
AFP rev. eca5cf0e4817

So far there are no observable deficiencies, but heavy users might want
to check whether everything is still fine.

The matter is quite brittle and so far not systematically tested.

Cheers,
Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Aug 11 2022 at 21:51):

From: "Achim D. Brucker" <adbrucker@0x5f.org>
Hi,
Thanks a lot. I just tested it with my (hopefully soon to be published)
project using the Real-setup and it works nicely.

One questions: the constant "*" (multiplication) is not defined
for OCaml. Is this intentional or an oversight?

Best,
Achim

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Dec 21 2024 at 16:20 UTC