cubical
cubical copied to clipboard
/Functions/FunExtEquiv.agda Error: Warning "Could not Generate equivalence
I'm running cubical agda and when loading any file I receive the following error:
/home/rymndbkr/agda/cubical/Cubical/Functions/FunExtEquiv.agda:110,3-111,86
Could not generate equivalence when splitting on indexed family,
the function will not compute on transports by a path.
Reason: UnsupportedYet Injectivity
position: 0
type: ℕ
datatype: ℕ
parameters:
indices:
constructor: suc
when checking the definition of rinv
I also receive similar errors but when checking the definition of other identifiers, such as "==", "elim", "++Fin", "head" and a buncd of others. The file is able to load and I am able to do some work in agda. I couldn't find anything elsewhere online about a problem like this so I thought I'd mention it here.
Just in case this is still relevant for anyone: This warning can be irgnored and it doesn't come up, if you check the library with Agda 2.6.2 -- which is now recommended in README.md.
So this warning doesn't have any effect on how the Cubical repository will operate on my computer? I'm also wondering, what causes the warning?