rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]

[Nils Anders Danielsson]

On 2016-01-27 23:45, Andreas Abel wrote:
> Note that your files do not check on current master (could be released
> as agda-2.5).  This is due to changes in the operator parser.  Also,
> some COMPILED pragmas have to be removed.

I've attached a potential fix for these issues.

I replaced one rewrite equality "eq" with "sym eq".

The code included an expression "ff imp b ≡ tt", where _imp_ was
infixr 4, and _≡_ infix 4. Previously infix 4 corresponded to a strictly
lower precedence than infixr 4. Now this kind of expression is rejected,
giving the user an opportunity to explain what it is supposed to mean by
inserting parentheses or changing fixities.

-- 
/NAD
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ial.diff
Type: text/x-patch
Size: 4593 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20160128/d7792463/ial.bin