search

math-comp / mczify

Micromega tactics for Mathematical Components
23 stars 8 forks source link

`N` forms a semiring #47

Closed pi8027 closed 1 year ago

pi8027 commented 1 year ago

I was trying to add a proper support for semirings in Algebra Tactics (on top of math-comp/algebra-tactics#71), and then found that this semiring instance would be useful for that.

I also wanted to add morphism instances for nat_of_bin and bin_of_nat, but it requires math-comp/math-comp#1031. Maybe I can just copy instances for nat from math-comp/math-comp#1031 to here.

proux01 commented 1 year ago

Could you add examples to test the new instances?

pi8027 commented 1 year ago

Will do.