[Agda] Error defining Universe Polymorphism

[Ashish Mishra]

Thanks Nils , that solves the problem .



On Fri, Oct 9, 2015 at 8:13 AM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2015-10-09 08:48, Ashish Mishra wrote:
>
>> I am facing a pertinent issue while defining new LEVELS of Universes
>> using the BUILTIN pragmas of Agda .
>>
>
> The mechanism used to introduce levels has changed:
>
>   https://github.com/agda/agda/blob/2.4.2.4/CHANGELOG#L3134-L3147
>   https://github.com/agda/agda/blob/2.4.2.4/CHANGELOG#L1156-L1210
>
> --
> /NAD
>



-- 
Regards,
Ashish Mishra
Graduate Student,
Computer Science and Automation Department,IISc
Cell : +91-9611194714
Mailto : ashishmishra at csa.iisc.ernet.in
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151009/4d239f39/attachment-0001.html