Changeset 2403 for Papers/polymorphic-variants-2012
- Timestamp:
- Oct 18, 2012, 3:57:33 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/polymorphic-variants-2012/test.ma
r2402 r2403 4 4 λb. match b with [ true ⇒ True | false ⇒ False ]. 5 5 6 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 7 6 8 inductive expr (E: Type[0]) : Type[0] ≝ 7 9 Num : nat -> expr E 8 | Plus : expr E -> exprE -> expr E9 | Mul : expr E -> exprE -> expr E.10 | Plus : E -> E -> expr E 11 | Mul : E -> E -> expr E. 10 12 11 13 inductive tag : Type[0] := num : tag | plus : tag | mul : tag. … … 38 40 { 39 41 se_el :> expr E; 40 se_el_in: bool_to_Prop (is_in … l se_el)42 se_el_in: is_in … l se_el 41 43 }. 42 44 … … 46 48 coercion mk_sub_expr : 47 49 ∀l:list tag.∀E.∀e:expr E. 48 ∀p: bool_to_Prop (is_in ? l e).sub_expr l E49 ≝ mk_sub_expr on e:expr Eto sub_expr ? ?.50 ∀p:is_in ? l e.sub_expr l E 51 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?. 50 52 51 53 (**************************************) 52 54 53 definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E. 55 definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝ 56 λE,f,e. 57 match e return λe. is_in … [plus] e → nat with 58 [ Plus x y ⇒ λH. f x + f y 59 | _ ⇒ λH:False. ? 60 ] (se_el_in ?? e). 61 elim H qed. 62 63 definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝ 64 λE,f,e. 65 match e return λe. is_in … [mul] e → nat with 66 [ Mul x y ⇒ λH. f x + f y 67 | _ ⇒ λH:False. ? 68 ] (se_el_in ?? e). 69 elim H qed. 70 71 definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝ 72 λE,f,e. 73 match e return λe. is_in … [plus;mul] e → nat with 74 [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) 75 | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) 76 | _ ⇒ λH:False. ? 77 ] (se_el_in ?? e). 78 [2,3: % | elim H] 79 qed.
Note: See TracChangeset
for help on using the changeset viewer.