[Agda-dev] Primitive.agda and UHC back-end

Ulf Norell ulf.norell at gmail.com
Mon Feb 15 13:44:17 CET 2016


I'm pretty sure we don't actually need the MAlonzo pragmas for levels.

/ Ulf

On Mon, Feb 15, 2016 at 1:35 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
wrote:

> Hi,
>
> Just out curiosity, why aren't UHC pragmas in Primitive.agda?
>
> Best,
>
> --
> Andrés
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20160215/11fd0383/attachment.html


More information about the Agda-dev mailing list