[Agda] Is there currently a Problem with the standard lib from git?

[stvienna wiener]

Sorry, was a false alarm. I did everything again in a virtual machine and
then it worked.

Steve

Am Fr., 1. Okt. 2021 um 20:31 Uhr schrieb stvienna wiener <
stvienna at gmail.com>:

> Dear all,
>
> I'm using the agda standard lib from git:
> commit 853e309e55bdc80407564e44396751a84e8c55f0
>
> ~/agda-stdlib/src/Data/Nat/DivMod.agda:205,1-47
> Agda.Primitive.Cubical.primTransp
> (λ i →
>    m /
>    Agda.Primitive.Cubical.primComp (λ i₁ → ℕ)
>    (λ i₁ .o →
>       Agda.Primitive.Cubical.primPOr
>       (Agda.Primitive.Cubical.primIMax
>        (Agda.Primitive.Cubical.primINeg i) φ)
>       i (λ .o₁ → suc m₁) (λ .o₁ → x i₁) _)
>    (suc m₁)
>    ≤ n / x₁ i)
> φ (/-mono-≤ x₂ (s≤s x₃)) is not usable at the required modality
> when checking the definition of /-mono-≤
>
> $ agda --version
> Agda version 2.6.3-78ea6d2
>
> Is this a known error, or is there a problem on my agda configuration?
>
> Thanks & regards
>
> Steve
> (from Vienna)
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211001/be117ef7/attachment.html>