From 0ed7fb39e919a6a4814dc5e9d435edf924cca72f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Sep 2006 15:59:21 +0000 Subject: [PATCH] added notation --- matita/library/datatypes/constructors.ma | 28 ++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) 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. -- 2.39.2