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

[Andreas Abel]

Maybe what is missing is a mechanism that declares postulates as --safe 
if they are connected to a BUILTIN.

This would involve changing --safe not to scream at each postulate 
immediately, but instead collecting postulates and scream only at the 
end of the file if some postulates have not been declared BUILTINs 
successfully.

On 15.02.2016 15:54, Ulf Norell wrote:
>
>
> On Mon, Feb 15, 2016 at 3:14 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co
> <mailto:asr at eafit.edu.co>> wrote:
>
>     On 15 February 2016 at 08:37, Ulf Norell <ulf.norell at gmail.com
>     <mailto:ulf.norell at gmail.com>> wrote:
>     > Clearly Agda.Primitive ought to be considered safe. Or is universe
>     > polymorphism not in the safe fragment?
>
>     Strictly speaking, Primitve.Agda isn't using universe polymorphism.
>
>
> No, but universe polymorphism requires builtin levels which need postulates.
>
> / Ulf
>
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>

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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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