[Agda] `abstract' on Web keywords

[Nils Anders Danielsson]

On 2013-05-14 12:38, Sergei Meshveliani wrote:
> Now, the obstacle is that all these lemmata are not at the top level,
> they are each inside its parametrized module, and usually, somewhere at
> the second level of `where'. And abstracting them out most often leads
> to "unsolved metas" at the type check.

If you use abstract, then the type signature is "frozen" before the body
is checked. This can be annoying, but ensures that implementation
details do not leak out. In your case I guess you do not care about such
leakage, because you use abstract for performance reasons, not to hide
implementation details. One possibility is to have two kinds of
abstract, one that is aimed at performance and one that is aimed at
information hiding. However, abstract is already a bit of a hack.

-- 
/NAD