From 1092af803d3d1a9788008d8abf6c7470d68f22c7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Sep 2010 16:27:48 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/sets/setoids.ma | 6 ++++++ helm/software/matita/nlibrary/sets/setoids1.ma | 10 ++++++++-- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma index c159be66a..b66f4d457 100644 --- a/helm/software/matita/nlibrary/sets/setoids.ma +++ b/helm/software/matita/nlibrary/sets/setoids.ma @@ -29,6 +29,8 @@ for @{ eq_rel ? (eq0 ?) $a $b }. interpretation "setoid symmetry" 'invert r = (sym ???? r). notation ".= r" with precedence 50 for @{'trans $r}. interpretation "trans" 'trans r = (trans ????? r). +notation > ".=_0 r" with precedence 50 for @{'trans_x0 $r}. +interpretation "trans_x0" 'trans_x0 r = (trans ????? r). nrecord unary_morphism (A,B: setoid) : Type[0] ≝ { fun1:1> A → B; @@ -40,6 +42,9 @@ notation "l ‡ r" with precedence 90 for @{'prop2 $l $r }. notation "#" with precedence 90 for @{'refl}. interpretation "prop1" 'prop1 c = (prop1 ????? c). interpretation "refl" 'refl = (refl ???). +notation "┼_0 c" with precedence 89 for @{'prop1_x0 $c }. +notation "l ╪_0 r" with precedence 89 for @{'prop2_x0 $l $r }. +interpretation "prop1_x0" 'prop1_x0 c = (prop1 ????? c). ndefinition unary_morph_setoid : setoid → setoid → setoid. #S1; #S2; @ (unary_morphism S1 S2); @; @@ -56,6 +61,7 @@ unification hint 0 ≔ o1,o2 ; carr X ≡ unary_morphism o1 o2. interpretation "prop2" 'prop2 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r). +interpretation "prop2_x0" 'prop2_x0 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r). nlemma unary_morph_eq: ∀A,B.∀f,g: unary_morphism A B. (∀x. f x = g x) → f=g. #A B f g H x1 x2 E; napply (.= †E); napply H; nqed. diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma index 4aac43e44..fb960c1db 100644 --- a/helm/software/matita/nlibrary/sets/setoids1.ma +++ b/helm/software/matita/nlibrary/sets/setoids1.ma @@ -48,15 +48,19 @@ for @{ eq_rel1 ? (eq1 ?) $a $b }. interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r). interpretation "setoid symmetry" 'invert r = (sym ???? r). notation ".= r" with precedence 50 for @{'trans $r}. +notation ".=_1 r" with precedence 50 for @{'trans_x1 $r}. interpretation "trans1" 'trans r = (trans1 ????? r). interpretation "trans" 'trans r = (trans ????? r). +interpretation "trans1_x1" 'trans_x1 r = (trans1 ????? r). nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝ { fun11:1> A → B; prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a') }. - + +notation "┼_1 c" with precedence 89 for @{'prop1_x1 $c }. interpretation "prop11" 'prop1 c = (prop11 ????? c). +interpretation "prop11_x1" 'prop1_x1 c = (prop11 ????? c). interpretation "refl1" 'refl = (refl1 ???). ndefinition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1. @@ -71,8 +75,10 @@ unification hint 0 ≔ S, T ; R ≟ (unary_morphism1_setoid1 S T) (* --------------------------------- *) ⊢ carr1 R ≡ unary_morphism1 S T. - + +notation "l ╪_1 r" with precedence 89 for @{'prop2_x1 $l $r }. interpretation "prop21" 'prop2 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r). +interpretation "prop21_x1" 'prop2_x1 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r). nlemma unary_morph1_eq1: ∀A,B.∀f,g: unary_morphism1 A B. (∀x. f x = g x) → f=g. /3/. nqed. -- 2.39.2