helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term".
  16
  17 (* POLARIZED TERMS
  18    - Naming policy:
  19      - natural numbers      : sorts h k, local references i j, lengths l o
  20      - boolean values       : p q
  21      - generic leaf items   : m n
  22      - generic binding items: r s
  23      - generic flat items   : r s
  24      - generic head items   : m n
  25      - terms                : t u
  26 *)
  27
  28 include "preamble.ma".
  29
  30 inductive Leaf: Set \def
  31    | sort: Nat \to Leaf
  32    | lref: Nat \to Leaf
  33 .
  34
  35 inductive Bind: Set \def
  36    | abbr: Bind
  37    | abst: Bind
  38    | excl: Bind
  39 .
  40
  41 inductive Flat: Set \def
  42    | appl: Flat
  43    | cast: Flat
  44 .
  45
  46 inductive IntB: Set \def
  47    | bind: Bool \to Bind \to IntB
  48 .
  49
  50 inductive IntF: Set \def
  51    | flat: Bool \to Flat \to IntF
  52 .
  53
  54 inductive Term: Set \def
  55    | leaf: Leaf \to Term
  56    | intb: IntB \to Term \to Term \to Term
  57    | intf: IntF \to Term \to Term \to Term
  58 .