matita/matita/lib/lambda-delta/language/term.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "lambda-delta/language/item.ma".
  13
  14 (* TERMS ********************************************************************)
  15
  16 (* 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 *)
  21 .
  22
  23 interpretation "sort (term)" 'Star k = (TSort k).
  24
  25 interpretation "local reference (term)" 'Weight i = (TLRef i).
  26
  27 interpretation "term construction (binary)" 'SCon I T1 T2 = (TCon2 I T1 T2).