[Agda] Error in stdlib Relation/Binary/Core.agda

Chantal KELLER chantal.keller at wanadoo.fr
Wed Sep 9 11:18:18 CEST 2009


Hello everybody,

Using emacs, when I try to load (C-c C-l) a file containing the
following two lines:

=================
module test where
open import Relation.Binary.Core
=================

I get the following error:

=================
/home/keller/agda-stdlib/Relation/Binary/Core.agda:52,15-15
/home/keller/agda-stdlib/Relation/Binary/Core.agda:52,15:
in the name _Preserves_?_, the part ? is not valid :<ERROR> forall
{av(1) av(2)} -> (av(1) -> av(2)) ...
=================

But I manage to compile this file in a terminal.

Thanks for your help,
-- 
Chantal KELLER


More information about the Agda mailing list