[Agda] $ in eq-reasoning

mechvel at scico.botik.ru mechvel at scico.botik.ru
Sat Sep 7 19:47:38 CEST 2019


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.

Thanks,

------
Sergei




More information about the Agda mailing list