From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 7 May 2010 21:20:58 +0000 (+0000)
Subject: notation
X-Git-Tag: make_still_working~2906
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=86b6c02aa918e5e7115f42947428590d5f0a26e6;p=helm.git

notation
---

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index c33dca9bd..f8916ee5a 100644
--- a/helm/software/matita/nlibrary/re/re.ma
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -120,7 +120,7 @@ nlet rec eclose (S: Type[0]) (E: pre S) on E ≝
      let E1' ≝ eclose ? E1 in
      let E1'' ≝ snd … E1' in
       match fst … E1' with
-       [ true =>
+       [ true ⇒ 
           let E2' ≝ eclose ? E2 in
            〈 fst … E2', pc ? E1'' (snd … E2') 〉
        | false ⇒ 〈 false, pc ? E1'' E2 〉 ]
@@ -310,6 +310,7 @@ nlet corec foo_nop (b: bool):
      | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
 nqed.
 
+(*
 nlet corec foo (a: unit):
  equiv NAT
   (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
@@ -329,21 +330,38 @@ nlet corec foo (a: unit):
      ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
   ##]
 nqed.
+*)
 
-ndefinition test1 ≝
- pc ? (pk ? (po ? (ps ? 0) (ps ? 1))) (ps ? 0).
-
-ndefinition test2 ≝
- po ?
-  (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0))
-  (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 1)).
-
-ndefinition test3 ≝
- pk ? (pc ? (pc ? (ps ? 0) (pk ? (pc ? (ps ? 0) (ps ? 1)))) (ps ? 1)).
+notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
+notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
+interpretation "star" 'pk a = (pk ? a).
+                      
+notation "❨a|b❩" non associative with precedence 90 for @{ 'po $a $b}.
+interpretation "or" 'po a b = (po ? a b).
+           
+notation < "a b" non associative with precedence 60 for @{ 'pc $a $b}.
+notation > "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
+interpretation "cat" 'pc a b = (pc ? a b).
+
+notation < "a" non associative with precedence 90 for @{ 'pp $a}.
+notation > "` term 90 a" non associative with precedence 90 for @{ 'pp $a}.
+interpretation "atom" 'pp a = (pp ? a).
+
+(* to get rid of \middot *)
+ncoercion rex_concat : ∀S:Type[0].∀p:pre S. pre S → pre S  ≝ pc
+on _p : pre ? to ∀_:?.?.
+(* we could also get rid of ` with a coercion from nat → pre nat *) 
+
+ndefinition test1 ≝ ❨ `0 | `1 ❩^* `0.
+ndefinition test2 ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
+ndefinition test3 ≝ (`0 (`0`1)^* `1)^*.
 
 nlemma foo: in_moves NAT
   [0;0;1;0;1;1] (eclose ? test3) = true.
+ nnormalize in match test3;
  nnormalize;
+//;
+nqed.
 
 (**********************************************************)