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

[Andreas Abel]

Agda-2.4.3 has different parsing rules than Agda-2.4.2. You have to use 
the 2.4.2.4 branch of the standard library with my version of agda 
(which is a modification of Agda-2.4.2.4).

On 20.11.2015 07:52, effectfully wrote:
> 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?
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/