Email Gateway (Aug 22 2022 at 12:09): Email Gateway (Aug 22 2022 at 12:09):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,
when adapting our theories to Isabelle2016-RC1, I encountered a problem with the new upgrade of typedef and the overloaded constants.
Note that ('a,'b)rbt in "~~/src/HOL/Library/RBT" is such an overloaded type. As a user of RBT’s I now have to put a context around
other types that use RBT’s with a parametric 'a as in the example type „use_rbt_A“.
However, the problem is that, I now cannot put these types into records or use records with generic RBT’s as arguments, since
records are not localized. So, the creation of both types use_rbt_B and use_rbt_C fails.
Is there any known work-around to this problem?
(Except for converting the records into datatypes and then recursively wrap a context with [[typedef_overloaded]] around every further
type declaration that transitively depends on these types)
With best regards,
René
theory Test
imports
"~~/src/HOL/Library/RBT"
begin
context
notes [[typedef_overloaded]]
begin
datatype 'a use_rbt_A = Foo "('a,bool) rbt"
end
record 'a use_rbt_B =
bar :: "'a use_rbt_A"
record 'a use_rbt_C =
com :: "('a,bool)rbt"
end
Email Gateway (Aug 22 2022 at 12:09):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi René,
The following does work
declare [[typedef_overloaded]]
record …
declare [[typedef_overloaded = false]]
But eventually the record package will be localized, and we won’t need such imperative declarations.
Dmitriy
Email Gateway (Aug 22 2022 at 12:12):From: "C. Diekmann" <diekmann@in.tum.de>
Dear René,
unfortunately, I have no answer to your question.
Thank you for sharing the 'context notes [[typedef_overloaded]]'
pattern to enable overloading for only one datatype definition. This
solves one of my problems
(http://article.gmane.org/gmane.science.mathematics.logic.isabelle.user/12503).
The following question remains:
Is using typedef_overloaded somehow dangerous?
Best Regards,
Cornelius
Last updated: Apr 19 2024 at 20:15 UTC