Changeset 1351 for src/Cminor


Ignore:
Timestamp:
Oct 11, 2011, 12:24:33 PM (9 years ago)
Author:
campbell
Message:

Tidy up some loose ends from the invariants branch merge.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Cminor/semantics.ma

    r1316 r1351  
    292292axiom UnknownLabel : String.
    293293axiom 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.
    307294
    308295definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
Note: See TracChangeset for help on using the changeset viewer.