[Agda] meta vars regression from version 2.3.2

Nils Anders Danielsson nad at cse.gu.se
Tue Sep 17 10:19:00 CEST 2013


On 2013-09-15 02:04, Christian Sattler wrote:
> Below is a self-contained code sample that initially loads
> successfully in interactive mode of the latest development version,
> highlighting the single hole in the last line (along with several
> instances of yellow). However, attempting to fill the hole with h
> results in the following message:
>
> An internal error has occurred. Please report this as a bug.
> Location of the error: src/full/Agda/TypeChecking/MetaVars.hs:654
>
> The hole-filling appears to work just fine under Agda 2.3.2.

http://code.google.com/p/agda/issues/detail?id=903

-- 
/NAD


More information about the Agda mailing list