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

[Andrés Sicard-Ramírez]

On 21 November 2015 at 10:40, Sergei Meshveliani <mechvel at botik.ru> wrote:
> I have installed  agda-issue-1692-master

I guess you are talking about 'agda-issue-1692' instead of
'agda-issue-1692-master'.

If you followed the instructions

>  git clone https://github.com/andreasabel/agda-issue-1692.git
>  cd agda-issue-1692
>  git checkout maint-2.4.2
>  make install-bin

the Agda executable is called agda-2.4.2.5, that is

  $ agda-2.4.2.5 --version
  Agda version 2.4.2.5

> For my application,
>
> /home/mechvel/agda/stLib/0.11/src/Data/Bool/Base.agda:28,1-43
> Multiple Haskell bindings for Data.Bool.Base.Bool. Note that
> builtin numbers, booleans, chars and strings don't need COMPILED
> pragmas.
>
> So, I do not know, so far, how to test  agda-issue-1692-master.

You are not using the Agda executable from agda-issue-1692.

-- 
Andrés