[Agda] type annotation in-place

Andrew Pitts Andrew.Pitts at cl.cam.ac.uk
Thu Oct 8 09:39:01 CEST 2015


>> The report is "Unsolved metas".
>> And without `abstract', it is type-checked.
>
>
> If you use abstract, then meta-variables in the type signature are
> frozen before the body is type-checked:
>
>   https://github.com/agda/agda/issues/418

Is Agda's "abstract" keyword documented/exlained anywhere? Clicking on
it at the page <http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Keywords>
takes one to the Modules documentation
<http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Modules>,
but searching for "abstract" on that page reveals no mention of this
keyword. :-(

Andy


More information about the Agda mailing list