From 798c509fb17048996eb30fb991cc2da21d07dfcb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Mar 2009 17:49:39 +0000 Subject: [PATCH] notation ++ --- helm/software/matita/tests/unifhint.ma | 37 +++++++++++++++++++++----- 1 file changed, 30 insertions(+), 7 deletions(-) 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. -- 2.39.2