matita/matita/lib/lambda-delta/language/item.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 (* THE FORMAL SYSTEM λδ - MATITA SOURCE SCRIPTS
  13  * Specification started: 2011 April 17
  14  * - Patience on me so that I gain peace and perfection! -
  15  * [ suggested invocation to start formal specifications with ]
  16  *)
  17
  18 include "lambda-delta/ground.ma".
  19
  20 (* BINARY ITEMS *************************************************************)
  21
  22 (* binary items *)
  23 inductive item2: Type[0] ≝
  24    | Abbr: item2 (* abbreviation *)
  25    | Abst: item2 (* abstraction *)
  26    | Appl: item2 (* application *)
  27    | Cast: item2 (* explicit type annotation *)
  28 .
  29
  30 (* reduction-related categorization *****************************************)
  31
  32 (* binary items entitled for theta reduction *)
  33 definition thable2 ≝ λI. I = Abbr.
  34
  35 (* binary items entitled for zeta reduction *)
  36 definition zable2 ≝ λI. I = Abbr ∨ I = Cast.