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

[Andrés Sicard-Ramírez]

On 15 February 2016 at 08:36, Andreas Abel <abela at chalmers.se> wrote:
> What is the problem with Primitive.agda?
>
> $ agda --safe Safe.agda
> Checking Safe (/home/abel/agda/test/bugs/Safe.agda).
> Finished Safe.
>
> What other output would you expect?

I'm using postulates. Why the --safe option didn't reject the module?

-- 
Andrés