Email Gateway (Aug 18 2022 at 17:54): Email Gateway (Aug 18 2022 at 17:54):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Hi all,
I have written a little ML library allowing to automatically prove, in most
cases, instantiations of types (typedefs, records and datatypes) as countable
(see ~~/src/HOL/Library/Countable). The style of the library is still a little
rough but I think it could be a nice addition to the Isabelle Library with
some more work, mostly for Imperative_HOL (~~/src/HOL/Imperative_HOL) which
can only store values of countable types in its heap.
However, as Lukas Bulwhan said to me, improving it and integrating it in
Isabelle while nobody use it would certainly be a lost of time.
So here is my question: would anybody be interested in this addition ?
I attach this library with a theory containing tests/examples.
Anyway, if you have some advices for improving it, they would be welcome.
Regards,
Mathieu Giorgino
Countable.ML
Countable_Examples.thy
Email Gateway (Aug 18 2022 at 17:55):From: Peter Lammich <peter.lammich@uni-muenster.de>
This is definitely a useful tool for ImperativeHOL ... One could
probably integrate
it into the datatype package, such that datatypes automatically become
countable (like Haskell infers some typeclasses automatically (on demand))
Peter
Mathieu Giorgino schrieb:
Last updated: Apr 20 2024 at 12:26 UTC