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

Andrés Sicard-Ramírez asr at eafit.edu.co
Mon Feb 15 15:03:51 CET 2016


On 15 February 2016 at 08:33, Andreas Abel <abela at chalmers.se> wrote:
> 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)


Touché!

-- 
Andrés


More information about the Agda-dev mailing list