[Agda-dev] One more point for my false-golfing score

[Wolfram Kahl]

On Wed, Jul 01, 2015 at 08:21:58AM +0200, Andreas Abel wrote:
> Subject: [Agda-dev] One more point for my false-golfing score
>
> -- https://code.google.com/p/agda/issues/detail?id=1599
> 
> data ⊥ : Set where
> 
> abstract
>

Nice to know that ``abstract'' is not only a premature optimisation,
but also unsound.

(I used ``abstract'' my early Agda2 days to get more theories
 trough my memory constraints, but as Agda got better,
 at some point its advantages essentially disappeared,
 and its disadvantages made me abandon it,
 so I am not using ``abstract'' anymore.
)

If you take out the ``abstract'' and the indentation,
you get a positivity-check error message that sounds like
it might be ``fixed'' even for continued use of ``abstract''...  ;-(


Wolfram