Re: [isabelle] How to extract the record from a locale?
Locales normally do not introduce a record type for the set of parameters they fix.
However, if you refer to the development in HOL/Algebra, there are record definitions in
the theories. For example, the record type is "'a ring" for the locale "ring". It is
defined at the top of ~~/src/HOL/Algebra/Ring.thy.
More precisely, the locales in HOL/Algebra use the extensible variant of the record types,
i.e, "('a, 'b) ring_scheme" instead of "'a ring". The additional type parameter 'b
represents all future field extensions of the record. It depends on your construction
whether you can work with arbitrary extensions or have to stick to the fixed set of
In Isabelle/jEdit You can find out about the types of the record by Ctrl-hovering over the
fixed variable at the locale declaration. Ctrl-Click on the type takes you to the record
Hope this helps,
On 10/07/14 10:25, Holden Lee wrote:
For example, given a locale like *ring*, I would like to get the type of
its record ('a set (carrier), 'a=>'a=>'a (mult),...), so that I can feed it
into a function that does an algebraic construction on rings.
definition polynomial_ring :: "<ring_record> => <ring_record>"
This archive was generated by a fusion of
Pipermail (Mailman edition) and