[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.



More information about the Agda mailing list