Changeset 2402 for Papers/polymorphic-variants-2012

Timestamp:

Oct 18, 2012, 3:36:50 PM (9 years ago)

Author:

sacerdot

Message:

Progress on parametric types.

File:

• Papers/polymorphic-variants-2012/test.ma (modified) (2 diffs)

Papers/polymorphic-variants-2012/test.ma

@@ -35 +35 @@
  λE,l,e. memb Tag (tag_of_expr ? e) l. 
 
-record sub_expr (E: Type[0]) (l: list tag) : Type[0] ≝
+record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝
 {
   se_el :> expr E;
@@ -41 +41 @@
 }.
 
-coercion sub_expr : ∀E:Type[0].∀l:list tag .Type[0]
- ≝ sub_expr on _l: list tag to Type[0].
+coercion sub_expr : ∀l:list tag. Type[0] → Type[0]
+ ≝ sub_expr on _l: list tag to Type[0] → Type[0].
 
 coercion mk_sub_expr :
- ∀E.∀l:list tag.∀e:expr E.
-  ∀p:bool_to_Prop (is_in ? l e).sub_expr E l
+ ∀l:list tag.∀E.∀e:expr E.
+  ∀p:bool_to_Prop (is_in ? l e).sub_expr l E
  ≝ mk_sub_expr on e:expr E to sub_expr ? ?.
 
 (**************************************)
 
-definition additive_expr : Type[0] ≝ [plus].
+definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E.