[Agda] -1 as identifier

Andrés Sicard-Ramírez asr at eafit.edu.co
Thu Oct 8 23:12:45 CEST 2015


On 8 October 2015 at 14:57, Sergei Meshveliani <mechvel at botik.ru> wrote:
> the Development Agda of October 8
>
> considers  `-1' as an illegal name in the type signature in
>
>   -1 : ℤ
>   -1 = -[1+ 0 ]
>
> Is this by occasion, or it is an intended rule?

Negative numerals cannot be identifiers any more, see

  https://github.com/agda/agda/issues/1609

-- 
Andrés


More information about the Agda mailing list