<div dir="ltr"><div><br></div><div>Sorry, was a false alarm. I did everything again in a virtual machine and then it worked.</div><div><br></div><div>Steve<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am Fr., 1. Okt. 2021 um 20:31 Uhr schrieb stvienna wiener <<a href="mailto:stvienna@gmail.com">stvienna@gmail.com</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Dear all,</div><div><br></div><div>I'm using the agda standard lib from git:<br>commit 853e309e55bdc80407564e44396751a84e8c55f0 <br><br></div><div>~/agda-stdlib/src/Data/Nat/DivMod.agda:205,1-47<br>Agda.Primitive.Cubical.primTransp<br>(λ i →<br>   m /<br>   Agda.Primitive.Cubical.primComp (λ i₁ → ℕ)<br>   (λ i₁ .o →<br>      Agda.Primitive.Cubical.primPOr<br>      (Agda.Primitive.Cubical.primIMax<br>       (Agda.Primitive.Cubical.primINeg i) φ)<br>      i (λ .o₁ → suc m₁) (λ .o₁ → x i₁) _)<br>   (suc m₁)<br>   ≤ n / x₁ i)<br>φ (/-mono-≤ x₂ (s≤s x₃)) is not usable at the required modality<br>when checking the definition of /-mono-≤<br></div><div><br>$ agda --version<br>Agda version 2.6.3-78ea6d2<br><br></div><div>Is this a known error, or is there a problem on my agda configuration?</div><div><br></div><div>Thanks & regards<br><br></div><div>Steve <br>(from Vienna)<br></div><div><br></div></div>
</blockquote></div>