Re: [isabelle] Question about locales



Hi Peter,

context L
begin
 interpretation concept1[aa bb]
end

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 supported.

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 parameter R):

  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


Clemens






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.