Skip to content

Mczify 1.5.0+2.0+8.16

Latest
Compare
Choose a tag to compare
@pi8027 pi8027 released this 12 Jul 09:48
· 14 commits to master since this release
9f330a0

Compatible with Mathematical Components 2.0 and Coq 8.16 to 8.17. The ssrZ library now provides semiring instances for nat1 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.

  1. 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