[Agda] type check cost

[Nils Anders Danielsson]

On 2015-10-07 21:42, Sergei Meshveliani wrote:
> It reports
>
> ------------------------------
> ...
> /home/mechvel/doconA/0.04/source/DPrelude.agda:275,46-63
> Don't know how to parse _~_ Respects2 _≈_. Could mean any one of:
>    _Respects2_ _~_ _≈_
>    _Respects2_ _~_ _≈_
> ...
>
> Operators used in the grammar:
>    Respects2 (infix operator, level 20) [_Respects2_
> (/home/mechvel/doconA/0.04/source/DPrelude.agda:245,1-12)]
> (the treatment of operators has changed,
> ...
> -----------------------------

Can you give a self-contained example?

> As I recall, there was a certain recent development version which
> required fixity decl for each operator.
> But  agda-2.4.2.4  has rejected this fixity requirement.
> Right?

Agda 2.4.2.4 was a maintenance release.

> Now, what have I to do, to set fixities everywhere in my (large) code?

We decided not to remove default fixities. However, some things have
changed. If you provide me with a small, self-contained example, then I
can perhaps help you.

-- 
/NAD