Changeset 1351 for src/Cminor
 Timestamp:
 Oct 11, 2011, 12:24:33 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/semantics.ma
r1316 r1351 292 292 axiom UnknownLabel : String. 293 293 axiom ReturnMismatch : String. 294 295 lemma Exists_exists : ∀A,P,l.296 Exists A P l →297 ∃x. P x.298 #A #P #l elim l [ *  #hd #tl #IH * [ #H %{hd} @H  @IH ]299 qed.300 301 lemma Exists_All : ∀A,P,Q,l.302 Exists A P l →303 All A Q l →304 ∃x. P x ∧ Q x.305 #A #P #Q #l elim l [ *  #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/  #H1 * #_ #H2 @IH // ]306 qed.307 294 308 295 definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
Note: See TracChangeset
for help on using the changeset viewer.