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

[Sergei Meshveliani]

On Fri, 2015-11-20 at 08:51 +0100, Andreas Abel wrote:
> 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).
> 


I have installed  agda-issue-1692-master  and  agda-stdlib-0.11.

For my application,

  agda $agdaLibOpt Int/Integer0.agda

starts with checking standard library:

Checking Int.Integer0
(/home/mechvel/doconA/0.04/source/Int/Integer0.agda).
  Skipping Level (/home/mechvel/agda/stLib/0.11/src/Level.agdai).
 Skipping Function (/home/mechvel/agda/stLib/0.11/src/Function.agdai).
 Checking Algebra.FunctionProperties
(/home/mechvel/agda/stLib/0.11/src/Algebra/FunctionProperties.agda).
  Checking Relation.Binary
(/home/mechvel/agda/stLib/0.11/src/Relation/Binary.agda).
     Skipping Data.Empty
(/home/mechvel/agda/stLib/0.11/src/Data/Empty.agdai).
    Skipping Relation.Nullary
(/home/mechvel/agda/stLib/0.11/src/Relation/Nullary.agdai).
   Skipping Data.Product
(/home/mechvel/agda/stLib/0.11/src/Data/Product.agdai).
   Checking Data.Sum (/home/mechvel/agda/stLib/0.11/src/Data/Sum.agda).
    Checking Data.Maybe.Base
(/home/mechvel/agda/stLib/0.11/src/Data/Maybe/Base.agda).
     Checking Data.Bool.Base
(/home/mechvel/agda/stLib/0.11/src/Data/Bool/Base.agda).
      Skipping Data.Unit.Base
(/home/mechvel/agda/stLib/0.11/src/Data/Unit/Base.agdai).
      Skipping Relation.Binary.Core
(/home/mechvel/agda/stLib/0.11/src/Relation/Binary/Core.agdai).

/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.

Regards,

------
Sergei