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.