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