X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FUnified%2FSUB%2FT%2Fdefs.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FUnified%2FSUB%2FT%2Fdefs.ma;h=df6e1945ef8a7f3d71b64f2acba603399b9e5358;hb=bc29be71041b83d3ff452d3dfe95b013f7d7bbe9;hp=798ace41d7340d1128fbeef7af7fb1e9fd7067ba;hpb=e2c7f456a6d13e86c720104db16c9b28e5933e18;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma
index 798ace41d..df6e1945e 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma
@@ -14,21 +14,27 @@
 
 (* Project started Tue Aug 22, 2006 ***************************************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/P/defs".
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Term/defs".
 
 (* POLARIZED TERMS
    - Naming policy:
-     - natural numbers      : sorts h k, local references i j, lengths l
-     - boolean values       : a b
-     - generic binding items: x
-     - generic flat items   : y
-     - generic head items   : z
-     - terms                : p q
+     - natural numbers      : sorts h k, local references i j, lengths l o
+     - boolean values       : p q
+     - generic leaf items   : m n
+     - generic binding items: r s 
+     - generic flat items   : r s
+     - generic head items   : m n
+     - terms                : t u
 *)
 
 include "../../RELATIONAL/Nat/defs.ma".
 include "../../RELATIONAL/Bool/defs.ma".
 
+inductive Leaf: Set \def
+   | sort: Nat \to Leaf
+   | lref: Nat \to Leaf
+.
+
 inductive Bind: Set \def
    | abbr: Bind
    | abst: Bind
@@ -41,12 +47,11 @@ inductive Flat: Set \def
 .
 
 inductive Head: Set \def
-   | bind: Bind \to Head
-   | flat: Flat \to Head
+   | bind: Bool \to Bind \to Head
+   | flat: Bool \to Flat \to Head
 .
 
-inductive P: Set \def
-   | sort: Nat \to P
-   | lref: Nat \to P
-   | head: Bool \to Head \to P \to P \to P
+inductive Term: Set \def
+   | leaf: Leaf \to Term
+   | head: Head \to Term \to Term \to Term
 .