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

[Andreas Abel]

Checking Safe (/home/abel/agda/test/bugs/Safe.agda).
/home/abel/agda/test/bugs/Safe.agda:2,1-11
The right-hand side can only be omitted if there is an absurd
pattern, () or {}, in the left-hand side.
when checking that the clause moduleSafe has type _1

:-E (feeling evil)

On 15.02.2016 13:22, Andrés Sicard-Ramírez wrote:
> moduleSafe where
>
>    open import Agda.Primitive
>
>    Foo : Set
>    Foo = Level

-- 
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/