X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fhelena%2Fexamples%2Fexp_math%2FT0.hln;h=fdc962d01fc50a5642163495e534e749704152b5;hb=edf9e34100f49d4aa5ba8f3ce53e34af7718d88e;hp=8321246c649a413a74e7a8401b24c7c8c39a611a;hpb=9c489fe144c562dca776df59264329b704e18c49;p=helm.git

diff --git a/helm/software/helena/examples/exp_math/T0.hln b/helm/software/helena/examples/exp_math/T0.hln
index 8321246c6..fdc962d01 100644
--- a/helm/software/helena/examples/exp_math/T0.hln
+++ b/helm/software/helena/examples/exp_math/T0.hln
@@ -4,67 +4,67 @@
 
 \open elements \* [1] 2.1. 2.2. 2.4. *\
 
-   \decl "rule application" App: *Obj => *Obj => *Obj -> *Prop
+   \decl "rule application" App: { [*Obj] [*Obj] [*Obj] } *Prop
 
-   \decl "classification predicate" Cl: *Obj -> *Prop
+   \decl "classification predicate" Cl: [*Obj] *Prop
 
-   \decl "classification membership" Eta: *Obj => *Obj -> *Prop
+   \decl "classification membership" Eta: { [*Obj] [*Obj] } *Prop
 
 \* we must make an explicit coercion from *Obj to *Term *\
-   \decl "object-to-term-coercion" T: *Obj -> *Term
+   \decl "object-to-term-coercion" T: [*Obj] *Term
 
-   \decl "term application" At: *Term => *Term -> *Term
+   \decl "term application" At: { [*Term] [*Term] } *Term
 
-   \decl "term-object equivalence" E: *Term => *Obj -> *Prop
+   \decl "term-object equivalence" E: { [*Term] [*Obj] } *Prop
 
 \close
 
 \open logical_abbreviations \* [1] 2.3. 2.5. *\
 
    \def "logical comprehension restricted to classifications"
-      CAll = [q:*Obj->*Prop] [x:*Obj] Cl(x) -> q(x)      
-           : (*Obj -> *Prop) -> *Prop
+      CAll = [q:[*Obj]^1 *Prop] All([x:*Obj]^2 Imp(Cl(x), q(x)))      
+           : [[*Obj]^1 *Prop] *Prop
 
    \def "logical existence restricted to classifications"
-      CEx = [q:*Obj->*Prop] Ex([x:*Obj] And(Cl(x), q(x)))      
-          : (*Obj -> *Prop) -> *Prop
+      CEx = [q:[*Obj]^1 *Prop] Ex([x:*Obj]^2 And(Cl(x), q(x)))      
+          : [[*Obj]^1 *Prop] *Prop
 
    \def "logical comprehension restricted to a classification"
-      EAll = [a:*Obj, q:*Obj->*Prop] [x:*Obj] Eta(x, a) -> q(x)      
-           : *Obj => (*Obj -> *Prop) -> *Prop
+      EAll = { [a:*Obj] [q:[*Obj]^1 *Prop] } All([x:*Obj]^2 Imp(Eta(x, a), q(x)))      
+           : { [*Obj] [[*Obj]^1 *Prop] } *Prop
 
    \def "logical existence restricted to a classification"
-      EEx = [a:*Obj, q:*Obj->*Prop] Ex([x:*Obj] And(Eta(x, a), q(x)))      
-          : *Obj => (*Obj -> *Prop) -> *Prop
+      EEx = { [a:*Obj] [q:[*Obj]^1 *Prop] } Ex([x:*Obj]^2 And(Eta(x, a), q(x)))
+          : { [*Obj] [[*Obj]^1 *Prop] } *Prop
 
 \close
 
 \open non_logical_abbreviations \* [1] 2.4. 2.7 *\
 
    \def "object application"
-      OAt = [f:*Obj, x:*Obj] At(T(f), T(x)) : *Obj => *Obj -> *Term
+      OAt = { [f:*Obj] [x:*Obj] } At(T(f), T(x)) : { [*Obj] [*Obj] } *Term
 
    \def "convergence of a term to an object"
-      Conv = [t:*Term] EX([y:*Obj] E(t, y)) : *Term -> *Prop
+      Conv = [t:*Term] EX([y:*Obj]^2 E(t, y)) : [*Term] *Prop
 
    \def "term-term equivalence"
-      Eq = [t1:*Term, t2:*Term] [y:*Obj] Iff(E(t1, y), E(t2, y))
-         : *Term => *Term -> *Prop
+      Eq = { [t1:*Term] [t2:*Term] } All([y:*Obj]^2 Iff(E(t1, y), E(t2, y)))
+         : { [*Term] [*Term] } *Prop
 
    \def "classification membership of a term"
-      TEta = [t:*Term, a:*Obj] EEx(a, [y:*Obj] E(t, y))
-           : *Term => *Obj -> *Prop
+      TEta = { [t:*Term] [a:*Obj] } EEx(a, [y:*Obj]^2 E(t, y))
+           : { [*Term] [*Obj] } *Prop
 
    \def "operation (rule with inhabited domain)"
-      Op = [f:*Obj] Ex([x:*Obj] Conv(OAt(f, x))) : *Obj -> *Prop
+      Op = [f:*Obj] Ex([x:*Obj]^2 Conv(OAt(f, x))) : [*Obj] *Prop
 
    \def "classification inclusion"
-      ESub = [a1:*Obj, a2:*Obj] EAll(a1, [x:*Obj] Eta(x, a2))
-           : *Obj => *Obj -> *Prop
+      ESub = { [a1:*Obj] [a2:*Obj] } EAll(a1, [x:*Obj]^2 Eta(x, a2))
+           : { [*Obj] [*Obj] } *Prop
 
     \def "classification morphism"
-      ETo = [f:*Obj, a:*Obj, b:*Obj] EAll(a, [x:*Obj] TEta(OAt(f, x), b))
-          : *Obj => *Obj => *Obj -> *Prop
+      ETo = { [f:*Obj] [a:*Obj] [ b:*Obj] } EAll(a, [x:*Obj]^2 TEta(OAt(f, x), b))
+          : { [*Obj] [*Obj] [*Obj] } *Prop
 
 \close
 
@@ -74,15 +74,15 @@
    \ax e_refl: [y:*Obj] E(T(y), y)
 
    \ax e_at_in: [t1:*Term][t2:*Term][f:*Obj][x:*Obj][y:*Obj] 
-                E(t1, f) -> E(t2, x) -> App(f, x, y) -> E(At(t1, t2), y) 
+                [E(t1, f)] [E(t2, x)] [App(f, x, y)] E(At(t1, t2), y) 
 \*
-   \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] E(At(T(f), T(x)), y) -> App(f,x,y) 
+   \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] [E(At(T(f), T(x)), y)] App(f, x, y) 
 *\
    \ax "I (i)" id_dec: [x:*Obj][y:*Obj] Or(Id(x, y), NId(x, y))
    
    \ax "I (ii)" at_mono: [f:*Obj][x:*Obj][y1:*Obj][y2:*Obj]
-                         E(OAt(f, x), y1) -> E(OAt(f, x), y2) -> Id(y1, y2)
+                         [E(OAt(f, x), y1)] [E(OAt(f, x), y2)] Id(y1, y2)
 
-   \ax "I (iii)" eta_cl: [x:*Obj][a:*Obj] Eta(x, a) -> Cl(a)
+   \ax "I (iii)" eta_cl: [x:*Obj][a:*Obj] [Eta(x, a)] Cl(a)
 
 \close