search

agda / cubical

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

Remove commutativity assumption to `bigOpSplit++` #997

Closed jpoiret closed 1 year ago

jpoiret commented 1 year ago

bigOpSplit++ only needs associativity.

jpoiret commented 1 year ago

The test failure seems to be related to a version mismatch between Cabal and GHC (Cabal is too old for GHC 9.6). The change is minimal so I don't expect any problems with this.

jpoiret commented 1 year ago

I'm focusing on fixing CI for now so I need my main branch for something else, I'll resend a PR later with another branch on my side :)