1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
16 * Specification started: 2011 April 17
17 * Confluence of context-sensitive parallel reduction closed: 2011 September 21
18 * Confluence of context-free parallel reduction closed: 2011 September 6
19 * - Patience on me so that I gain peace and perfection! -
20 * [ suggested invocation to start formal specifications with ]
23 include "Ground_2/list.ma".
24 include "Ground_2/star.ma".
25 include "Basic_2/notation.ma".
27 (* ITEMS ********************************************************************)
30 inductive item0: Type[0] ≝
31 | Sort: nat → item0 (* sort: starting at 0 *)
32 | LRef: nat → item0 (* reference by index: starting at 0 *)
35 (* binary binding items *)
36 inductive bind2: Type[0] ≝
37 | Abbr: bind2 (* abbreviation *)
38 | Abst: bind2 (* abstraction *)
41 (* binary non-binding items *)
42 inductive flat2: Type[0] ≝
43 | Appl: flat2 (* application *)
44 | Cast: flat2 (* explicit type annotation *)
48 inductive item2: Type[0] ≝
49 | Bind: bind2 → item2 (* binding item *)
50 | Flat: flat2 → item2 (* non-binding item *)
53 coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2.
55 coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2.
57 (* Basic_1: removed theorems 19:
58 s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc
60 r_S r_plus r_plus_sym r_minus r_dis s_r r_arith0 r_arith1