[Agda] Typechecking failure for Agda Standard Library

Dirk Ullrich dirk.ullrich at googlemail.com
Tue May 31 14:57:17 CEST 2011


Hallo,

when I try to generate the Agda interface files for the current darcs
version of Standard Library with the current darcs version of Agda I
get the following error:


Checking Data.BoundedVec
(/msysts/common/packages/build/agda2lib/build/devel.sandbox/src/Data/BoundedVec.agda).

Unsolved metas at the following locations:
  /msysts/common/packages/build/agda2lib/build/devel.sandbox/src/Data/BoundedVec.agda:57,5-10
  /msysts/common/packages/build/agda2lib/build/devel.sandbox/src/Data/BoundedVec.agda:57,13-58,29
  /msysts/common/packages/build/agda2lib/build/devel.sandbox/src/Data/BoundedVec.agda:54,26-31
  /msysts/common/packages/build/agda2lib/build/devel.sandbox/src/Data/BoundedVec.agda:69,11-16
  /msysts/common/packages/build/agda2lib/build/devel.sandbox/src/Data/BoundedVec.agda:69,58-59
  /msysts/common/packages/build/agda2lib/build/devel.sandbox/src/Data/BoundedVec.agda:69,19-59
  /msysts/common/packages/build/agda2lib/build/devel.sandbox/src/Data/BoundedVec.agda:67,26-31

May be this is a general bug.
Dirk


More information about the Agda mailing list