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

Chantal KELLER chantal.keller at wanadoo.fr
Thu Sep 10 09:39:44 CEST 2009


Nils Anders Danielsson a écrit :
> 
> On 2009-09-09 10:18, Chantal KELLER wrote:
>> =================
>> /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)) ...
>> =================
> 
> It seems as if you are using an old version of the standard library. In
> recent versions of Agda the symbol → is reserved, so _Preserves_→_ has
> been renamed to _Preserves_⟶_.
> 
> The standard library documentation specifies, for every release, which
> version of Agda it has been tested with.
> 

Ok, it seems that the Debian package is out of date. I will download the
version that corresponds to my version of Agda.
-- 
Chantal KELLER


More information about the Agda mailing list