[Agda] Cannot type-check Level.agda in the Agda standard library with the current Agda 2.2.11 (command line)

[Arseniy Alekseyev]

I think you have not updated the agda executable. You need to install
it from src/main/Agda-executable.cabal in Agda source.

On 22 September 2011 06:28, IKEGAMI Daisuke <ikegami.da at gmail.com> wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>