X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Falgebra%2Fmagmas.ma;h=685d6248059afb3e162ae4ec00ea1304f05318af;hb=14aa468ded0030440dbc9cc8fb5b936d927bb6fd;hp=8ca0254b4387e4655c791043da7c9fce29c111ae;hpb=9114e57d5273c6f6072ad5867e4d1503c89ae059;p=helm.git diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index 8ca0254b4..685d62480 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -16,7 +16,7 @@ include "sets/sets.ma". nrecord magma_type : Type[1] ≝ { mtcarr:> setoid; - op: binary_morphism mtcarr mtcarr mtcarr + op: unary_morphism mtcarr (unary_morph_setoid mtcarr mtcarr) }. nrecord magma (A: magma_type) : Type[1] ≝