[Agda] running out of memory in formalization of category theory

[kahl at cas.mcmaster.ca]

Nils Anders Danielsson wrote:
 > 
 > > We sometimes proved those theorems, then postulated the proofs and
 > > referred to the postulated proofs, just in order to avoid Agda
 > > normalising the proofs.
 > 
 > You don't need to use postulates. Use abstract instead:
 > 
 >    abstract
 > 
 >      foo : Foo
 >      foo = …
 > 
 >      bar : Bar
 >      bar = …
 > 
 > Here foo and bar are transparent within the abstract block (within all
 > abstract blocks in the same module, I believe ①), but opaque outside.

This is the first time I learn about ``abstract'' in Agda,
which got me wondering: Where is ``abstract'' documented?
The first relevant place I found on the wiki is

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VisibilityAndEvaluation

, which says:

 | Few people seem to be aware of the issues raised above, or the presence of
 | abstract, and some discussion about abstraction would be nice. 

Too true, even today!

There is also a partial specification in

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Bugs.20070616-1

 | If a definition d is abstract, then the following guarantee should apply:
 | 
 |   * As long as the type signature of d is unchanged its implementation
 |     can be changed in any way without statically affecting code outside
 |     of the abstraction barrier (the behaviour of a running program can of
 |     course be affected). 

But there is nothing in the reference manual.


Ulf's thesis already includes ``abstract'' in the list of reserved words,
but, at least by searching through the PDF, I could not find any related
explanation.


Is there more documentation of ``abstract'' anywhere?


Wolfram