X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fexamples%2Fexp_math%2FL.hln;h=6d6c4a68377d782925ba525bf6fde86c9e91d152;hb=c44a7c4d35c1bb9651c3596519d8262e52e90ff4;hp=4b84f65fd8fa0bd88b22e2ca48e7df2229b46f9a;hpb=95872555aaa040a22ad2d93cb1278f79e20da70c;p=helm.git

diff --git a/helm/software/helena/examples/exp_math/L.hln b/helm/software/helena/examples/exp_math/L.hln
index 4b84f65fd..6d6c4a683 100644
--- a/helm/software/helena/examples/exp_math/L.hln
+++ b/helm/software/helena/examples/exp_math/L.hln
@@ -6,37 +6,37 @@
 
    \decl "logical false" False: *Prop
 
-   \decl "logical conjunction" And: *Prop => *Prop -> *Prop
+   \decl "logical conjunction" And: { [*Prop] [*Prop] } *Prop
 
-   \decl "logical disjunction" Or: *Prop => *Prop -> *Prop
+   \decl "logical disjunction" Or: { [*Prop] [*Prop] } *Prop
 
 \* implication and non-dependent abstraction are isomorphic *\
    \def "logical implication" 
-      Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
+      Imp = { [p:*Prop] [q:*Prop] } [p]^1 q : { [*Prop] [*Prop] } *Prop
 
 \* comprehension and dependent abstraction are isomorphic *\
    \def "unrestricted logical comprehension"
-      All = [q:*Obj->*Prop] [x:*Obj] q(x) : (*Obj -> *Prop) -> *Prop
+      All = [q:[*Obj]^1 *Prop] [x:*Obj]^1 q(x) : [[*Obj]^1 *Prop] *Prop
 
-   \decl "unrestricted logical existence" Ex: (*Obj -> *Prop) -> *Prop
+   \decl "unrestricted logical existence" Ex: [[*Obj]^1 *Prop] *Prop
 
-   \decl "syntactical identity" Id: *Obj => *Obj -> *Prop
+   \decl "syntactical identity" Id: { [*Obj] [*Obj] } *Prop
 
 \close
 
 \open abbreviations \* [1] 2.3. *\
 
    \def "logical negation" 
-      Not = [p:*Prop] p -> False : *Prop -> *Prop
+      Not = [p:*Prop] Imp(p, False) : [*Prop] *Prop
 
    \def "logical equivalence"
-      Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
+      Iff = { [p:*Prop] [q:*Prop] } And(Imp(p, q), Imp(q, p)) : { [*Prop] [*Prop] } *Prop
 
    \def "unrestricted strict logical existence"
-      EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
-         : (*Obj -> *Prop) -> *Prop
+      EX = [p:[*Obj]^1 *Prop] Ex([x:*Obj]^2 And(p(x), All([y:*Obj]^2 Imp(p(y), Id(x, y)))))
+         : [[*Obj]^1 *Prop] *Prop
 
    \def "negated syntactical identity"
-      NId = [x:*Obj, y:*Obj] Not(Id(x, y)) : *Obj => *Obj -> *Prop
+      NId = { [x:*Obj] [y:*Obj] } Not(Id(x, y)) : { [*Obj] [*Obj] } *Prop
 
 \close