Primitive.agda [was [Agda-dev] Agda and Packages/Libraries]

[Ulf Norell]

>
> For example, given
>
>   module Safe where
>
>   open import Agda.Primitive
>
>   Foo : Set
>   Foo = Level
>
> Which should be the output of
>
>   $ agda --safe Safe.agda
>

Clearly Agda.Primitive ought to be considered safe. Or is universe
polymorphism not in the safe fragment?

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20160215/3677a7ba/attachment-0001.html