From: Claudio Sacerdoti Coen Date: Thu, 30 Jul 2009 12:18:26 +0000 (+0000) Subject: More \ldots. X-Git-Tag: make_still_working~3591 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=70893c71a58e7788b9ec2256dd96f3d75818b61a;p=helm.git More \ldots. --- diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index caf903ae1..74663f45a 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -26,7 +26,7 @@ nrecord magma (A: magma_type) : Type[1] ≝ nrecord magma_morphism_type (A,B: magma_type) : Type ≝ { mmcarr:1> A → B; - mmprop: ∀x,y. mmcarr (op ? x y) = op ? (mmcarr x) (mmcarr y) + mmprop: ∀x,y. mmcarr (op … x y) = op … (mmcarr x) (mmcarr y) }. nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type ≝ @@ -38,7 +38,7 @@ ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝ λA,B,f,Sa. {y | ∃x. x ∈ Sa ∧ f x = y}. ndefinition mm_image: - ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma B. + ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism … Ma Mb → magma B. #A; #B; #Ma; #Mb; #f; napply (mk_magma …) [ napply (image … f Ma) @@ -56,7 +56,7 @@ ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝ λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}. ndefinition mm_counter_image: - ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma A. + ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism … Ma Mb → magma A. #A; #B; #Ma; #Mb; #f; napply (mk_magma …) [ napply (counter_image … f Mb) diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma index 9d31b0943..40982a660 100644 --- a/helm/software/matita/nlibrary/sets/setoids.ma +++ b/helm/software/matita/nlibrary/sets/setoids.ma @@ -18,13 +18,13 @@ include "properties/relations.ma". nrecord setoid : Type[1] ≝ { carr:> Type; eq: carr → carr → CProp; - refl: reflexive ? eq; - sym: symmetric ? eq; - trans: transitive ? eq + refl: reflexive … eq; + sym: symmetric … eq; + trans: transitive … eq }. ndefinition proofs: CProp → setoid. -#P; napply (mk_setoid ?????); +#P; napply (mk_setoid …); ##[ napply P; ##| #x; #y; napply True; ##|##*: nwhd; nrepeat (#_); napply I; @@ -33,17 +33,17 @@ nqed. nrecord function_space (A,B: setoid): Type ≝ { f:1> A → B; - f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a')) + f_ok: ∀a,a':A. proofs (eq … a a') → proofs (eq … (f a) (f a')) }. notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }. ndefinition function_space_setoid: setoid → setoid → setoid. - #A; #B; napply (mk_setoid ?????); + #A; #B; napply (mk_setoid …); ##[ napply (function_space A B); -##| #f; #f1; napply (∀a:A. proofs (eq ? (f a) (f1 a))); +##| #f; #f1; napply (∀a:A. proofs (eq … (f a) (f1 a))); ##| nwhd; #x; #a; - napply (f_ok ? ? x ? ? ?); (* QUI!! *) + napply (f_ok … x …); (* QUI!! *) (* unfold carr; unfold proofs; simplify; apply (refl A) | simplify;