- the example is now minimal so the bug is understood.

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / test.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
index aac04467bace657625aa5f1eb8ed62bbd6c8552c..1f4fac570da00244a59ed15e141889837735c4e1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
@@ -14,38 +14,26 @@
 
 universe constraint Type[0] < Type[1].
 
-(* notations ****************************************************************)
-
 notation "hvbox(a break \to b)"
   right associative with precedence 20
 for @{ \forall $_:$a.$b }.
 
-notation "hvbox( T . break ⓑ { term 46 I } break term 48 T1 )"
- non associative with precedence 47
- for @{ 'DxBind2 $T $I $T1 }.
-
-(* definitions **************************************************************)
-
-inductive lenv: Type[0] ≝
-| LAtom: lenv
-| LPair: lenv → lenv → lenv → lenv
-.
+notation "hvbox( * )"
+ non associative with precedence 90
+ for @{ 'B }.
 
-inductive genv: Type[0] ≝
-| GAtom: genv
-| GPair: genv → genv → genv → genv
-.
+inductive l: Type[0] ≝ L: l.
 
-axiom fw: genv → lenv → Prop.
+inductive g: Type[0] ≝ G: g.
 
-(* interpretations **********************************************************)
+axiom f: l → Prop.
 
-interpretation "environment binding construction (binary)"
-   'DxBind2 L I T = (LPair L I T).
+interpretation "b" 'B = L.
 
-interpretation "environment binding construction (binary)"
-   'DxBind2 G I T = (GPair G I T).
+interpretation "b" 'B = G.
 
-(* statements ***************************************************************)
+(* FG: two interpretations of the same notation and with the same description
+       override eachother, so the description is not just informative
+*)
 
-axiom fw_shift: ∀I,G,K,V. fw G (K.ⓑ{I}V).
+axiom s: f *.