[Agda] `abstract' on Web keywords

[Sergei Meshveliani]

On Tue, 2013-05-14 at 11:22 +0200, Nils Anders Danielsson wrote:
> On 2013-05-14 10:32, Sergei Meshveliani wrote:
> > But clicking at `abstract'  displays several sections on modules where I
> > do not find the word `abstract'.
> > Am I missing something?
> 
> I don't think there is much documentation of abstract in the
> (incomplete) reference manual.
> 

1. I have searched through the two manuals, and have not found any
`abstract' (I skip the expressions like "to abstract over").   

2. I have searched in  lib-0.7/src
(not all, though)
and have found only 4 abstract decls -- in BoundedVec*, as I recall.

3. I thought that in my application almost all lemma proofs can be
abstracted. Because other parts are not likely to analyze the structure
of the corresponding proof data (they could, but I do not see a reason
for arranging this in these particular cases).
But I may have a wrong idea about `abstract'.

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. 

One of such attempt has even lead to the checker hung for 30 minutes.  

Another attempt of abstracting out a couple of middle size proofs in 
one module (which takes most of the space in type check) has lead to
reducing the space 7 times -- I cannot imagine, why.

Generally, I have an impression that I misuse `abstract', and the
program becomes incorrect, and the checker not always notices this.

4. Need I to move the lemma function being abstracted to the top level,
 to move from its parametrized module, with giving it the corresponding
additional arguments ?
(so that the lemma will unfold the prelude environment independently).

Thanks,

------
Sergei