[Agda] Cannot type-check Level.agda in the Agda standard library
with the current Agda 2.2.11 (command line)
IKEGAMI Daisuke
ikegami.da at gmail.com
Thu Sep 22 07:28:13 CEST 2011
Hello,
I got the following error message:
% cd lib/src
% agda -i . Level.agda
Checking Level (/Users/ikegami/works/AgdaLib/lib/src/Level.agda).
/Users/ikegami/works/AgdaLib/lib/src/Level.agda:27,1-32
Level is not an inductive data type
when checking the pragma BUILTIN LEVEL Level
Any suggestion?
It prevents generating HTML documents and compiling a file with MAlonzo
when I use the command agda.
On the other hand, emacs interface of Agda works well; does not complain.
I use agda on the HEAD at the darcs repository; the library is also on the HEAD.
Cheers,
Ike
More information about the Agda
mailing list