Changeset 2520 for Papers/polymorphicvariants2012/test.ma
 Timestamp:
 Dec 3, 2012, 4:07:45 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/test.ma
r2514 r2520 26 26  Mul _ _ => mul ]. 27 27 28 (*29 28 definition Q_holds_for_tag: 30 ∀E:Type[0]. ∀ l: list tag. ∀Q: ∀x: l E → Prop. ∀t:tag. memb … t l →Prop ≝31 λE, l,Q,t. ?.32 match t return λt. memb … t l → Propwith33 [ num ⇒ λH. (∀n. Q (Num … n))34  plus ⇒ λH. (∀x,y. Q (Plus … x y))35  mul ⇒ λH. (∀x,y. Q (Mul … x y))29 ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop ≝ 30 λE,Q,t. 31 match t with 32 [ num ⇒ ∀n. Q (Num … n) 33  plus ⇒ ∀x,y. Q (Plus … x y) 34  mul ⇒ ∀x,y. Q (Mul … x y) 36 35 ]. 37 36 38 39 definition Q_holds_for_tag: 40 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. memb … t l → Prop ≝ 41 λE,l,Q,t. ?. 42 match t return λt. memb … t l → Prop with 43 [ num ⇒ λH. (∀n. Q (Num … n)) 44  plus ⇒ λH. (∀x,y. Q (Plus … x y)) 45  mul ⇒ λH. (∀x,y. Q (Mul … x y)) 46 ]. 47 48 axiom Q_holds_for_tag_spec: 49 ∀E:Type[0]. ∀fixed_l: list tag. ∀Q: fixed_l E → Prop. ∀t:tag. 50 ∀p:memb … t fixed_l. Q_holds_for_tag … Q … p → 51 ∀x: [t] E. Q x. 52 *) 37 theorem Q_holds_for_tag_spec: 38 ∀E:Type[0]. ∀Q: expr E → Prop. 39 ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x. 40 #E #Q * normalize // 41 qed.
Note: See TracChangeset
for help on using the changeset viewer.