X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdatatypes%2Fconstructors.ma;h=d8130d714d1ac75f6d8e52c851ff5dd8eafe743b;hb=85857e1832b921fdba61be9e7fbfc81da50f38f6;hp=dd2a1760b9c640c7853fafbeb33babe2d7670ad2;hpb=b715c8a42bd126e4b11b8b72451d6497ce1f7f73;p=helm.git diff --git a/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma index dd2a1760b..d8130d714 100644 --- a/helm/software/matita/library/datatypes/constructors.ma +++ b/helm/software/matita/library/datatypes/constructors.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/datatypes/constructors/". include "logic/equality.ma". inductive void : Set \def. @@ -25,15 +24,9 @@ pair : A \to B \to Prod A B. interpretation "Pair construction" 'pair x y = (cic:/matita/datatypes/constructors/Prod.ind#xpointer(1/1/1) _ _ x y). -notation "hvbox(\langle x break , y \rangle )" with precedence 89 -for @{ 'pair $x $y}. - interpretation "Product" 'product x y = (cic:/matita/datatypes/constructors/Prod.ind#xpointer(1/1) x y). -notation "hvbox(x break \times y)" with precedence 89 -for @{ 'product $x $y}. - definition fst \def \lambda A,B:Type.\lambda p: Prod A B. match p with [(pair a b) \Rightarrow a]. @@ -42,20 +35,15 @@ definition snd \def \lambda A,B:Type.\lambda p: Prod A B. match p with [(pair a b) \Rightarrow b]. -interpretation "First projection" 'fst x = - (cic:/matita/datatypes/constructors/fst.con _ _ x). - -notation "\fst x" with precedence 89 -for @{ 'fst $x}. - -interpretation "Second projection" 'snd x = - (cic:/matita/datatypes/constructors/snd.con _ _ x). - -notation "\snd x" with precedence 89 -for @{ 'snd $x}. +interpretation "pair pi1" 'pi1 = (fst _ _). +interpretation "pair pi2" 'pi2 = (snd _ _). +interpretation "pair pi1" 'pi1a x = (fst _ _ x). +interpretation "pair pi2" 'pi2a x = (snd _ _ x). +interpretation "pair pi1" 'pi1b x y = (fst _ _ x y). +interpretation "pair pi2" 'pi2b x y = (snd _ _ x y). theorem eq_pair_fst_snd: \forall A,B:Type.\forall p:Prod A B. -p = 〈 (\fst p), (\snd p) 〉. +p = 〈 \fst p, \snd p 〉. intros.elim p.simplify.reflexivity. qed. @@ -68,4 +56,4 @@ interpretation "Disjoint union" 'plus A B = inductive option (A:Type) : Type ≝ None : option A - | Some : A → option A. \ No newline at end of file + | Some : A → option A.