[Agda-dev] 2.4.4 roadmap

[Andreas Abel]

On 28.09.2015 10:34, Ulf Norell wrote:
> What are other things we should consider?

The change in the operator parser that breaks any Agda development 
should not be released yet, imho.  I am not convinced of its merits 
compared to the breakage it causes.

I am for postponing the release of the new operator parsing.  Sections 
depend on it, but are they already stable? (There are issues with 
bloated error messages.)  I am not happy with how situations like TERM 
INFIX PREFIX TERM are handled without fixity declarations.

This is (when sufficiently stable) something for a next major version of 
Agda 2, imho.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/