Changeset 2404
 Timestamp:
 Oct 18, 2012, 4:10:56 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/test.ma
r2403 r2404 64 64 λE,f,e. 65 65 match e return λe. is_in … [mul] e → nat with 66 [ Mul x y ⇒ λH. f x +f y66 [ Mul x y ⇒ λH. f x * f y 67 67  _ ⇒ λH:False. ? 68 68 ] (se_el_in ?? e). … … 78 78 [2,3: %  elim H] 79 79 qed. 80 81 definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝ 82 λE,f,e. 83 match e return λe. is_in … [plus;mul;num] e → nat with 84 [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) 85  Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) 86  Num n ⇒ λH. n 87 ] (se_el_in ?? e). 88 % qed. 89 90 (*CSC: not accepted :( 91 inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const. 92 *) 93 94 inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr. 95 96 coercion K. 97 98 let rec eval_final_expr e on e : nat ≝ 99 match e with 100 [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e']. 101 cases e' try #x try #y % 102 qed. 103 104 example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6. 105 % qed.
Note: See TracChangeset
for help on using the changeset viewer.