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

stvienna wiener stvienna at gmail.com
Fri Oct 1 20:31:45 CEST 2021


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/58214007/attachment.html>


More information about the Agda mailing list