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 universe constraint Type[0] < Type[1].
17 (* notations ****************************************************************)
19 notation "hvbox(a break \to b)"
20 right associative with precedence 20
21 for @{ \forall $_:$a.$b }.
23 notation "hvbox( T . break ⓑ { term 46 I } break term 48 T1 )"
24 non associative with precedence 47
25 for @{ 'DxBind2 $T $I $T1 }.
27 (* definitions **************************************************************)
29 inductive lenv: Type[0] ≝
31 | LPair: lenv → lenv → lenv → lenv
34 inductive genv: Type[0] ≝
36 | GPair: genv → genv → genv → genv
39 axiom fw: genv → lenv → Prop.
41 (* interpretations **********************************************************)
43 interpretation "environment binding construction (binary)"
44 'DxBind2 L I T = (LPair L I T).
46 interpretation "environment binding construction (binary)"
47 'DxBind2 G I T = (GPair G I T).
49 (* statements ***************************************************************)
51 axiom fw_shift: ∀I,G,K,V. fw G (K.ⓑ{I}V).