Agda 2.6.0 compatibility
Opened this issue · 5 comments
ice1000 commented
Agda 2.6.0 compatibility
ice1000 commented
Checking Web.Semantic.Everything (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/Everything.agda).
Checking Web.Semantic.DL.ABox (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda).
Checking Web.Semantic.DL.ABox.Interp.Meet (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Meet.agda).
Checking Web.Semantic.DL.ABox.Interp.Morphism (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda).
Checking Web.Semantic.DL.TBox.Interp.Morphism (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/TBox/Interp/Morphism.agda).
Checking Web.Semantic.DL.ABox.Model (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda).
/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:143,1-14
Don't know how to parse inb (f , I⊨A). Could mean any one of:
inb (_,_ f I⊨A)
inb (_,_ f I⊨A)
inb (_,_ f I⊨A)
inb (_,_ f I⊨A)
inb (_,_ f I⊨A)
inb (_,_ f I⊨A)
Operators used in the grammar:
, (infixr operator, level 4) [_,_ (/home/ice/.cabal/share/x86_64-linux-ghc-8.4.3/Agda-2.6.0/lib/prim/Agda/Builtin/Sigma.agda:8,15-18)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda:15,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp.agda:14,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:25,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:68,3-6)]
, (infixr operator, level 5) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:139,5-8)]
when scope checking the left-hand side inb (f , I⊨A) in the
definition of inb
ice1000 commented
Is Agda completely losing the ability to use type inference to resolve overloaded operators? @UlfNorell Is this a language change?
ice1000 commented
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
((pipe (J , j)) (K , k)) (J≲K , j≲k)
Operators used in the grammar:
, (infixr operator, level 4) [_,_ (/home/ice/.cabal/share/x86_64-linux-ghc-8.4.3/Agda-2.6.0/lib/prim/Agda/Builtin/Sigma.agda:8,15-18)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda:15,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp.agda:14,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:25,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:68,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Morphism.agda:25,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Morphism.agda:30,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Morphism.agda:77,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Object.agda:13,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Integrity.agda:44,5-8)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Integrity.agda:65,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Integrity.agda:84,5-8)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/KB.agda:10,3-6)]
, (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/TBox.agda:14,3-6)]
, (infixr operator, level 5) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:139,5-8)]
when scope checking the left-hand side
pipe (J , j) (K , k) (J≲K , j≲k) in the definition of pipe
ice1000 commented
My Agda compiler is built from 2d980891f570cf4a50b8e8843eb9c5269b4d888e commit in the compiler repo
gallais commented
If you make sure that all _,_ have the same fixity level then it should fix the issue, I believe.