Changeset 2402 for Papers/polymorphic-variants-2012
- Timestamp:
- Oct 18, 2012, 3:36:50 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/polymorphic-variants-2012/test.ma
r2400 r2402 35 35 λE,l,e. memb Tag (tag_of_expr ? e) l. 36 36 37 record sub_expr ( E: Type[0]) (l: list tag) : Type[0] ≝37 record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝ 38 38 { 39 39 se_el :> expr E; … … 41 41 }. 42 42 43 coercion sub_expr : ∀ E:Type[0].∀l:list tag .Type[0]44 ≝ sub_expr on _l: list tag to Type[0] .43 coercion sub_expr : ∀l:list tag. Type[0] → Type[0] 44 ≝ sub_expr on _l: list tag to Type[0] → Type[0]. 45 45 46 46 coercion mk_sub_expr : 47 ∀ E.∀l:list tag.∀e:expr E.48 ∀p:bool_to_Prop (is_in ? l e).sub_expr E l47 ∀l:list tag.∀E.∀e:expr E. 48 ∀p:bool_to_Prop (is_in ? l e).sub_expr l E 49 49 ≝ mk_sub_expr on e:expr E to sub_expr ? ?. 50 50 51 51 (**************************************) 52 52 53 definition additive_expr : Type[0] ≝ [plus].53 definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E.
Note: See TracChangeset
for help on using the changeset viewer.