Compatible with Mathematical Components 2.0 and Coq 8.16 to 8.17. The ssrZ
library now provides semiring instances for nat
1 and N
, and homomorphism instances for Posz
,1 bin_of_nat
, nat_of_bin
, N.of_nat
, N.to_nat
, Z.of_nat
, and Z.of_N
.
-
These instances will also be included in MathComp from its version 2.1. Thus, we expect to eventually remove them from the Mczify library. ↩ ↩2