Changeset 2019 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Jun 6, 2012, 6:24:43 PM (9 years ago)
Author:
campbell
Message:

Split out special induction principle for Clight from soundness file.
Put cast simplification into compiler.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1988 r2019  
    269269lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
    270270#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
    271 
    272 (* We define a special induction principle tailored to the recursive definition
    273    above. *)
    274 
    275 definition is_not_lvalue: expr_descr → Prop ≝
    276 λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
    277 
    278 definition Plvalue ≝ λP:(expr → Prop).λe,ty.
    279 match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
    280271
    281272(* TODO: Can we do this sensibly with a map combinator? *)
Note: See TracChangeset for help on using the changeset viewer.