[Agda] private fields in records?

jleivent at comcast.net jleivent at comcast.net
Sat Feb 25 20:24:18 CET 2012

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

More information about the Agda mailing list