1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "Basic-2/grammar/item.ma".
17 (* TERMS ********************************************************************)
20 inductive term: Type[0] ≝
21 | TSort: nat → term (* sort: starting at 0 *)
22 | TLRef: nat → term (* reference by index: starting at 0 *)
23 | TPair: item2 → term → term → term (* binary item construction *)
26 interpretation "sort (term)" 'Star k = (TSort k).
28 interpretation "local reference (term)" 'LRef i = (TLRef i).
30 interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).
32 interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2).
34 interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2).