[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