Unified: refactoring

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Unified / SUB / T / defs.ma

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 798ace41d7340d1128fbeef7af7fb1e9fd7067ba..df6e1945ef8a7f3d71b64f2acba603399b9e5358 100644 (file)
--- 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
 .