2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "lambda-delta/language/item.ma".
14 (* TERMS ********************************************************************)
17 inductive term: Type[0] ≝
18 | TSort: nat → term (* sort: starting at 0 *)
19 | TLRef: nat → term (* reference by index: starting at 0 *)
20 | TCon2: item2 → term → term → term (* binary construction *)
23 interpretation "sort (term)" 'Star k = (TSort k).
25 interpretation "local reference (term)" 'Weight i = (TLRef i).
27 interpretation "term construction (binary)" 'SCon I T1 T2 = (TCon2 I T1 T2).