Re: [isabelle] Question about locales
interpretation concept1[aa bb]
does not work. Neither does:
interpretation L \<subseteq> concept1[aa bb]
Neither of these, although desirable, are supported by the current
implementation. In particular, note that on the rhs of \<subseteq>
you may only have a locale expression. Square brackets are not
I quote from an earlier message on this list, which explains how to
deal with such a sitution.
Here is an example. Assume that you have a locale for rings (for
simplicity, all operations of the ring are bundled in a singe
locale ring = fixes R assumes ...
and a constructor for polynomials Poly, which takes R to its
polynomial ring. You cannot have
interpretation ring < ring "Poly R"
since the right side is not a locale expression. Instead the
comment suggests the following: extend ring
locale poly_ring = ring + fixes P defines "P == Poly R"
and now you can make the interpretation
interpretation poly_ring < ring P
This archive was generated by a fusion of
Pipermail (Mailman edition) and