- we shared the atomic term constructions

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / grammar / term.ma

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma
index 309df0b3f6b2e910977456c4cb521184d93afaac..3b6614361654328f5548874c8edc738713f32fbb 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma
@@ -18,14 +18,15 @@ include "Basic-2/grammar/item.ma".
 
 (* terms *)
 inductive term: Type[0] ≝
-| TSort: nat → term                 (* sort: starting at 0 *)
-| TLRef: nat → term                 (* reference by index: starting at 0 *)
-| TPair: item2 → term → term → term (* binary item construction *)
+  | TAtom: item0 → term               (* atomic item construction *)
+  | TPair: item2 → term → term → term (* binary item construction *)
 .
 
-interpretation "sort (term)" 'Star k = (TSort k).
+interpretation "sort (term)" 'Star k = (TAtom (Sort k)).
 
-interpretation "local reference (term)" 'LRef i = (TLRef i).
+interpretation "local reference (term)" 'LRef i = (TAtom (LRef i)).
+
+interpretation "term construction (atomic)" 'SItem I = (TAtom I).
 
 interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).