search

agda / cubical

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

Introduce Semiring and refactor finite sums #1042

Closed felixwellen closed 11 months ago

felixwellen commented 11 months ago

So far, we only have CommSemiring. I don't have a Semiring that is not commutative, but I want to move the definition of sum from Ring to a place where it can also be used for Nat.

felixwellen commented 11 months ago

@mzeuner can you review this changes?