Changeset 2404 for Papers


Ignore:
Timestamp:
Oct 18, 2012, 4:10:56 PM (7 years ago)
Author:
sacerdot
Message:

Example finished.

File:
1 edited

Legend:

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

    r2403 r2404  
    6464 λE,f,e.
    6565  match e return λe. is_in … [mul] e → nat with
    66   [ Mul x y ⇒ λH. f x + f y
     66  [ Mul x y ⇒ λH. f x * f y
    6767  | _ ⇒ λH:False. ?
    6868  ] (se_el_in ?? e).
     
    7878[2,3: % | elim H]
    7979qed.
     80
     81definition 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 :-(
     91inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const.
     92*)
     93
     94inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr.
     95
     96coercion K.
     97
     98let 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'].
     101cases e' try #x try #y %
     102qed.
     103
     104example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6.
     105% qed.
Note: See TracChangeset for help on using the changeset viewer.