[Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!

effectfully effectfully at gmail.com
Fri Nov 20 07:52:14 CET 2015


Andrés Sicard-Ramírez, Andreas Abel, thanks for the solutions, I chose
the first.

I installed agda-issue-1692 and agda-stdlib-master and got parse errors here:

https://github.com/agda/agda-stdlib/blob/master/src/Data/Bool/Base.agda#L32
https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Base.agda#L31
https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/N-ary.agda#L52

Agda also complains about sections:

    Not in scope:
      _∘ at ...
    when scope checking _∘

Am I doing something wrong?


More information about the Agda mailing list