(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term".
-
(* POLARIZED TERMS
- Naming policy:
- 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 "preamble.ma".
-
-inductive Leaf: Set \def
- | sort: Nat \to Leaf
- | lref: Nat \to Leaf
-.
+include "Unified-Sub/preamble.ma".
-inductive Bind: Set \def
+inductive Bind: Type \def
| abbr: Bind
| abst: Bind
| excl: Bind
.
-inductive Flat: Set \def
+inductive Flat: Type \def
| appl: Flat
| cast: Flat
.
-inductive IntB: Set \def
+inductive IntB: Type \def
| bind: Bool \to Bind \to IntB
.
-inductive IntF: Set \def
+inductive IntF: Type \def
| flat: Bool \to Flat \to IntF
.
-inductive Term: Set \def
- | leaf: Leaf \to Term
+inductive Term: Type \def
+ | sort: Nat \to Term
+ | lref: Nat \to Term
| intb: IntB \to Term \to Term \to Term
| intf: IntF \to Term \to Term \to Term
.