Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [isabelle-dev] Countable instantiation addition


view this post on Zulip Email Gateway (Aug 18 2022 at 17:55):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
It does not work for any datatype (for example as soon as a non-countable type
is used in the datatype) but it could be integrated in the datatype package
with some checks.

However, I don't know if the time penalty (which isn't so big but there
anyway) on a so much used feature worth the benefit... unless it would be
present as an option (perhaps even with a recursive call on included non-
instantiated types). And an option would be mostly equivalent to (in fact even
less flexible than) a new command or an ML call subsequent to the datatype
definition.

Mathieu

Le jeudi 21 juillet 2011 19:02:41 Peter Lammich a écrit :


Last updated: Mar 28 2024 at 12:29 UTC