[Agda] Error defining Universe Polymorphism

Nils Anders Danielsson nad at cse.gu.se
Fri Oct 9 10:13:18 CEST 2015


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


More information about the Agda mailing list