Ignore:
Timestamp:
Oct 18, 2012, 3:36:50 PM (7 years ago)
Author:
sacerdot
Message:

Progress on parametric types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/test.ma

    r2400 r2402  
    3535 λE,l,e. memb Tag (tag_of_expr ? e) l.
    3636
    37 record sub_expr (E: Type[0]) (l: list tag) : Type[0] ≝
     37record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝
    3838{
    3939  se_el :> expr E;
     
    4141}.
    4242
    43 coercion sub_expr : ∀E:Type[0].∀l:list tag .Type[0]
    44  ≝ sub_expr on _l: list tag to Type[0].
     43coercion sub_expr : ∀l:list tag. Type[0] → Type[0]
     44 ≝ sub_expr on _l: list tag to Type[0] → Type[0].
    4545
    4646coercion mk_sub_expr :
    47  ∀E.∀l:list tag.∀e:expr E.
    48   ∀p:bool_to_Prop (is_in ? l e).sub_expr E l
     47 ∀l:list tag.∀E.∀e:expr E.
     48  ∀p:bool_to_Prop (is_in ? l e).sub_expr l E
    4949 ≝ mk_sub_expr on e:expr E to sub_expr ? ?.
    5050
    5151(**************************************)
    5252
    53 definition additive_expr : Type[0] ≝ [plus].
     53definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E.
Note: See TracChangeset for help on using the changeset viewer.