<div dir="ltr">As Andres said in his email, and as stated in the standard library README you need to use the `development` branch of the library rather the `master` branch with the release candidate.<div>Best,</div><div>Matthew</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Dec 29, 2019 at 7:39 PM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2019-12-22 14:41, Andres Sicard Ramirez wrote:<br>
> [..]<br>
> The Agda Team is very pleased to announce the first release candidate<br>
> of Agda 2.6.1.<br>
> [..]<br>
> The RC has been tested with GHC 8.8.1, 8.6.5, 8.4.4, 8.2.2 and 8.0.2.<br>
> [..]<br>
> Standard library<br>
> ==========<br>
> <br>
> For the time being, you can use the *experimental* branch of the<br>
> standard library which is compatible with the RC. This branch is<br>
> available at<br>
> <br>
>     <a href="https://github.com/agda/agda-stdlib/" rel="noreferrer" target="_blank">https://github.com/agda/agda-stdlib/</a><br>
> [..]<br>
<br>
<br>
I tried it on  ghc-8.6.3 under Ubuntu Linux 18.04 on a certain small <br>
application<br>
List0.agda:<br>
<br>
   > agda $agdaLibOpt List0.agda<br>
<br>
As I guess, it first starts type-checking the needed part of the <br>
"installed"<br>
master library of December 29. And it reports<br>
<br>
Checking List0 (/home/mechvel/inAgda/bfLib/0.3/List0.agda).<br>
  Checking Data.List.Relation.Unary.All.Properties <br>
(/home/mechvel/agda/stLib/master-dec29/src/Data/List/Relation/Unary/All/Properties.agda).<br>
   Checking Data.List.Membership.Propositional.Properties <br>
(/home/mechvel/agda/stLib/master-dec29/src/Data/List/Membership/Propositional/Properties.agda).<br>
    Checking Data.List.Relation.Unary.Any.Properties <br>
(/home/mechvel/agda/stLib/master-dec29/src/Data/List/Relation/Unary/Any/Properties.agda).<br>
/home/mechvel/agda/stLib/master-dec29/src/Data/List/Relation/Unary/Any/Properties.agda:251,16-27<br>
B.b != q₁ of type Level<br>
when checking that the inferred type of an application<br>
   Any.map _f_1489 y∈ys ≡ pq′<br>
matches the expected type<br>
   Any.map (λ q₂ → p , q₂) (Any.map (λ x₁ → P.subst Q x₁ _1452) y∈ys)<br>
   ≡ pq′<br>
<br>
--<br>
SM<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>