From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 11 Mar 2009 09:47:54 +0000 (+0000)
Subject: more examples
X-Git-Tag: make_still_working~4162
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c7605859c88549b8a812a19b85b3bbba53182ada;p=helm.git

more examples
---

diff --git a/helm/software/matita/tests/unifhint.ma b/helm/software/matita/tests/unifhint.ma
index 6e6900f80..42e9f6878 100644
--- a/helm/software/matita/tests/unifhint.ma
+++ b/helm/software/matita/tests/unifhint.ma
@@ -53,9 +53,9 @@ non associative with precedence 90 for
 @{ let ${ident a} ≝ $b in $c }.
 
 unification hint 0 (∀g:group.∀x:Expr.∀G:list (gcarr g). 
-
+           V ≟ 〚x,G〛
 (* ------------------------------------ *)
-       〚Eopp x,G〛 = 〚x,G〛^-1).
+       〚Eopp x,G〛 = V^-1).
 
 
 unification hint 0 (∀g:group.∀x,y.∀G:list (gcarr g). 
@@ -79,7 +79,14 @@ unification hint 3 (∀g:group.∀G:list (gcarr g).∀n.∀x:gcarr g.
 
                V ≟ 〚Evar n, G〛 
 (* ------------------------------------ *)  
-       〚(Evar (S n)), (x :: G)〛 = V) . 
+       〚(Evar (S n)), (x :: G)〛 = V) .
+       
+(* Esempio banale di divergenza       
+unification hint 0 (∀g:group.∀G:list (gcarr g).∀x.
+     V ≟ 〚x,G〛 
+ ------------------------------------      
+      〚x,G〛 = V).
+*)
 
 lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)). 
    start g ? ? h.