[Agda] $ in eq-reasoning

[mechvel at scico.botik.ru]

On 2019-09-07 20:47, mechvel at scico.botik.ru wrote:
> Who knows, please,
> why ``$`` is not type-checked when inserted into terms in the left
> column of the equality reasoning chain?
> For example,
> ```
> begin
>   f $ g x  ≈⟨ proof ⟩
>   x
> ∎
> ```
> Probably this concerns the relation between the precedence of ``$``
> and the precedence of the reasoning combinators.

More precisely it is expressed as

   "... when inserted at the _top_ of a term in the left column ...".

And as ``$`` is accepted at the lower levels, the subject becomes not so 
important.
Please, withdraw it.

--
SM