[Agda] type annotation in-place

[Nils Anders Danielsson]

On 2015-10-08 09:39, Andrew Pitts wrote:
> Is Agda's "abstract" keyword documented/exlained anywhere?

Yes, but perhaps not on the wiki.

Once I wrote this:

   The basic idea is that it should be possible to replace the
   "right-hand sides" of abstract definitions with /anything/ that
   type-checks, and this should not affect the type-checking of any
   definition outside of the given "abstract block" in any way.

In practice abstract is mostly used to stop definitions from unfolding.

-- 
/NAD