matita/matita/lib/lambda-delta/syntax/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/syntax/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 | TPair: item2 → term → term → term (* binary item 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)" 'SItem I T1 T2 = (TPair I T1 T2).
  28
  29 interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2).
  30
  31 interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2).