[Agda] private fields in records?

Andreas Abel andreas.abel at ifi.lmu.de
Sun Feb 26 12:28:59 CET 2012

This is a bug, I filed it as issue 580.

Each record declaration creates a module, with the corresponding privacy 

If privacy was take seriously, you should also never be able to 
construct record r (where you set the private field to 42).


On 25.02.12 8:24 PM, jleivent at comcast.net wrote:
> 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
> _______________________________________________ Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list