[isabelle] Local types do not work in for declarations of locales
Dear localisation experts,
I have a locale with polymorphic parameters and would like instantiate the type variables
in a sublocale. I know of two ways to achieve this:
1. Declare the parameters in a for clause with the specialised types.
2. Use the context element constrains with the specialised types.
From past discussions on this mailing list, I have the impression that "constrains" is
considered outdated and should be replaced with for clauses (for example in
I now ran into a problem with approach 1 when there are local type synonyms. Below is a
minimal example. Locale l declares a type with a type variable, its sublocale l1 fixes a
parameter whose type contains the local type, and l1's sublocale l2 tries to instantiate
type type variable:
locale l begin
typedef 'a td = "UNIV :: 'a set" ..
locale l1 = l + fixes y :: "'a td"
locale l2 = l1 y for y :: "bool td"
Here, I get an error in the last line claiming that td was an undefined type name. The
declaration works if I use constrains instead of a for clause.
locale l2 = l1 + constrains y :: "bool td"
Alternatively, I can go via the foundational type, but this seems to be somewhat ugly.
locale l2 = l1 y for y :: "bool l.td"
Is this a known limitation of localised typedef/type_synonym and/or a valid reason for
using the "deprecated" constrains element?
This archive was generated by a fusion of
Pipermail (Mailman edition) and