[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