Changeset 2019 for src/Clight/Cexec.ma
 Timestamp:
 Jun 6, 2012, 6:24:43 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Cexec.ma
r1988 r2019 269 269 lemma P_res_to_P: ∀A,P,e,v. P_res A P e → e = OK A v → P v. 270 270 #A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed. 271 272 (* We define a special induction principle tailored to the recursive definition273 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 ].280 271 281 272 (* TODO: Can we do this sensibly with a map combinator? *)
Note: See TracChangeset
for help on using the changeset viewer.