[Agda] private fields in records?

[jleivent at comcast.net]

The Agda documentation doesn't actually say that a record field can be private, but it allows the syntax.  And, as one would expect, declaring a field private prevents the field's associated projector function from being defined (or, at least it is not in scope outside the record).  However, there still are ways to get at the "private" field from outside the record, as the attached code shows.

One would think this is a bug, if only based on analogy between modules (where privacy is more fully documented) and records.

-- Jonathan Leivent
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PrivateBug.agda
Type: application/octet-stream
Size: 519 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120225/93403c61/PrivateBug.obj