We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 6f1dee6 commit 1ceb6eaCopy full SHA for 1ceb6ea
tests/monoid_law_structure.v
@@ -15,4 +15,6 @@ HB.mixin Record isPreMonoid T := {
15
HB.structure Definition PreMonoid := { T of isPreMonoid T }.
16
17
HB.structure Definition Monoid :=
18
- { T of isPreMonoid T & isMonLaw T zero add }.
+ { T of isPreMonoid T &
19
+ isMonLaw T zero add }.
20
+ (* isMonLaw T (@zero (PreMonoid.clone T _)) (@add (PreMonoid.clone T _))*)
0 commit comments