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

[Andreas Abel]

Dear Ike,

In the head, levels are postulates instead of a datatype as it used to be.

If you run

   make install-bin

from the Agda root directory then both the Agda-2.2.11 library and 
executables should be compiled and installed in your .cabal/bin directory.

Cheers,
Andreas

On 22.09.11 7:31 AM, Arseniy Alekseyev wrote:
> 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
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/