search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
456 stars 139 forks source link

/Functions/FunExtEquiv.agda Error: Warning "Could not Generate equivalence #711

Open morphismz opened 2 years ago

morphismz commented 2 years ago

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.

felixwellen commented 2 years ago

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.

morphismz commented 2 years ago

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?