From 9114e57d5273c6f6072ad5867e4d1503c89ae059 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Oct 2009 14:35:30 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/algebra/magmas.ma | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index 3e4cb942b..8ca0254b4 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -20,13 +20,13 @@ nrecord magma_type : Type[1] ≝ }. nrecord magma (A: magma_type) : Type[1] ≝ - { mcarr:> qpowerclass A; + { mcarr:> ext_powerclass A; op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr }. alias symbol "hint_decl" = "hint_decl_Type2". unification hint 0 ≔ - A : ? ⊢ carr1 (qpowerclass_setoid A) ≡ qpowerclass A. + A : ? ⊢ carr1 (ext_powerclass_setoid A) ≡ ext_powerclass A. (* ncoercion mcarr' : ∀A. ∀M: magma A. carr1 (qpowerclass_setoid (mtcarr A)) @@ -79,7 +79,7 @@ nqed. ndefinition m_intersect: ∀A. magma A → magma A → magma A. #A; #M1; #M2; napply (mk_magma …) - [ napply (intersect_ok ? M1 M2) + [ napply (intersect_is_ext_morph ? M1 M2) | #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2; napply conj; napply op_closed; nassumption ] nqed. \ No newline at end of file -- 2.39.2