From c7605859c88549b8a812a19b85b3bbba53182ada Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 11 Mar 2009 09:47:54 +0000 Subject: [PATCH] more examples --- helm/software/matita/tests/unifhint.ma | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) 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. -- 2.39.2