From: Enrico Tassi Date: Thu, 21 Sep 2006 15:59:21 +0000 (+0000) Subject: added notation X-Git-Tag: 0.4.95@7852~1012 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0ed7fb39e919a6a4814dc5e9d435edf924cca72f;p=helm.git added notation --- diff --git a/matita/library/datatypes/constructors.ma b/matita/library/datatypes/constructors.ma index 3f74db5ad..3567dd915 100644 --- a/matita/library/datatypes/constructors.ma +++ b/matita/library/datatypes/constructors.ma @@ -20,6 +20,18 @@ inductive void : Set \def. inductive Prod (A,B:Set) : Set \def 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:Set.\lambda p: Prod A B. match p with [(pair a b) \Rightarrow a]. @@ -28,8 +40,20 @@ definition snd \def \lambda A,B:Set.\lambda p: Prod A B. match p with [(pair a b) \Rightarrow b]. -theorem eq_pair_fst_snd: \forall A,B:Set.\forall p: Prod A B. -p = pair A B (fst A B p) (snd A B p). +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}. + +theorem eq_pair_fst_snd: \forall A,B:Set.\forall p:Prod A B. +p = 〈 (\fst p), (\snd p) 〉. intros.elim p.simplify.reflexivity. qed.