Changeset 1876 for src/common


Ignore:
Timestamp:
Apr 4, 2012, 6:48:26 PM (8 years ago)
Author:
campbell
Message:

Update Cexec soundness proof.
Change finishes_with predicate to inductive form so that qed no longer
spends huge amounts of time typechecking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r1231 r1876  
    9292| witness : ∀a:A. result A a.
    9393
    94 definition finishes_with : int → ∀S.res (snapshot S) → Prop ≝
    95 λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
     94inductive finishes_with : int → ∀S.res (snapshot S) → Prop ≝
     95fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)).
    9696
    9797include "common/Mem.ma".
Note: See TracChangeset for help on using the changeset viewer.