From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 10 Mar 2009 17:49:39 +0000 (+0000)
Subject: notation ++
X-Git-Tag: make_still_working~4166
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=798c509fb17048996eb30fb991cc2da21d07dfcb;p=helm.git

notation ++
---

diff --git a/helm/software/matita/tests/unifhint.ma b/helm/software/matita/tests/unifhint.ma
index 6d0c73350..6e6900f80 100644
--- a/helm/software/matita/tests/unifhint.ma
+++ b/helm/software/matita/tests/unifhint.ma
@@ -48,15 +48,38 @@ axiom P : ∀g:group. gcarr g → Prop.
 axiom tac : Expr → Expr.
 axiom start : ∀g,x,G.P g 〚x,G〛 → Prop.
 
-notation "@ t" non associative with precedence 90 for @{ (λx.x) $t }.
+notation > "ident a ≟ term 90 b term 20 c" 
+non associative with precedence 90 for 
+@{ let ${ident a} ≝ $b in $c }.
 
+unification hint 0 (∀g:group.∀x:Expr.∀G:list (gcarr g). 
 
-unification hint 0 (∀g:group.∀x:Expr.∀G:list (gcarr g). 〚Eopp x,G〛 = (@〚x,G〛) ^-1).
-unification hint 0 (∀g:group.∀x,y.∀G:list (gcarr g). 〚Emult x y,G〛 = (@〚x,G〛) * (@〚y,G〛)).
-unification hint 0 (∀g:group.∀G:list (gcarr g). 〚Eunit,G〛 = 𝟙).
-unification hint 2 (∀g:group.∀G:list (gcarr g).∀x:gcarr g. 〚(Evar 0), (x :: G)〛 = @x).
-unification hint 3 (∀g:group.∀G:list (gcarr g).∀n.∀x:gcarr g.(@〚Evar n, G〛)=
-   (〚(Evar (S n)), (x :: G)〛) ) . 
+(* ------------------------------------ *)
+       〚Eopp x,G〛 = 〚x,G〛^-1).
+
+
+unification hint 0 (∀g:group.∀x,y.∀G:list (gcarr g). 
+
+       V1 ≟ 〚x,G〛        V2 ≟ 〚y,G〛
+(* ------------------------------------ *) 
+           〚Emult x y,G〛 = V1 * V2).
+        
+unification hint 0 (∀g:group.∀G:list (gcarr g). 
+
+(* ------------------------------------ *)
+              〚Eunit,G〛 = 𝟙).
+
+unification hint 2 (∀g:group.∀G:list (gcarr g).∀x:gcarr g. 
+
+                   V ≟ x 
+(* ------------------------------------ *)
+          〚(Evar 0), (x :: G)〛 = V).
+  
+unification hint 3 (∀g:group.∀G:list (gcarr g).∀n.∀x:gcarr g.
+
+               V ≟ 〚Evar n, G〛 
+(* ------------------------------------ *)  
+       〚(Evar (S n)), (x :: G)〛 = V) . 
 
 lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)). 
    start g ? ? h.