Email Gateway (Aug 19 2022 at 11:02): Email Gateway (Aug 19 2022 at 11:02):From: Makarius <makarius@sketis.net>
On Sun, 19 May 2013, Randy Pollack wrote:
Is it correct that you cannot define a record in the context of a
locale?
The record package is still not localized, so it is confined to old-style
global theory contexts. In principle it could be as local as 'typedef'
(i.e. with the same limitations), but it has not been done yet.
If so, is there a commonly used work around that is not so verbose as
nested products?
Logically, a local record definition cannot depend on context parameters /
premsises anyway, so the difference is again just one of name spaces etc.
You can pull your record definition in front of all your other definition,
and let it stand as global theory specification for now.
Makarius
Email Gateway (Aug 19 2022 at 11:08):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Is it correct that you cannot define a record in the context of a locale?
If so, is there a commonly used work around that is not so verbose as
nested products?
Thanks,
Randy
Last updated: Nov 21 2024 at 12:39 UTC