# Changeset 2403

Ignore:
Timestamp:
Oct 18, 2012, 3:57:33 PM (8 years ago)
Message:

More work, example almost finished up to recursive type.

File:
1 edited

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

 r2402 λb. match b with [ true ⇒ True | false ⇒ False ]. coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. inductive expr (E: Type[0]) : Type[0] ≝ Num : nat -> expr E | Plus : expr E -> expr E -> expr E | Mul : expr E -> expr E -> expr E. | Plus : E -> E -> expr E | Mul : E -> E -> expr E. inductive tag : Type[0] := num : tag | plus : tag | mul : tag. { se_el :> expr E; se_el_in: bool_to_Prop (is_in … l se_el) se_el_in: is_in … l se_el }. coercion mk_sub_expr : ∀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 ? ?. ∀p:is_in ? l e.sub_expr l E ≝ mk_sub_expr on e:expr ? to sub_expr ? ?. (**************************************) definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E. definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝ λE,f,e. match e return λe. is_in … [plus] e → nat with [ Plus x y ⇒ λH. f x + f y | _ ⇒ λH:False. ? ] (se_el_in ?? e). elim H qed. definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝ λE,f,e. match e return λe. is_in … [mul] e → nat with [ Mul x y ⇒ λH. f x + f y | _ ⇒ λH:False. ? ] (se_el_in ?? e). elim H qed. definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝ λE,f,e. match e return λe. is_in … [plus;mul] e → nat with [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) | _ ⇒ λH:False. ? ] (se_el_in ?? e). [2,3: % | elim H] qed.
Note: See TracChangeset for help on using the changeset viewer.