[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