Changeset 2218 for src/common


Ignore:
Timestamp:
Jul 19, 2012, 6:45:49 PM (8 years ago)
Author:
campbell
Message:

Separate out cost properties required of RTLabs programs from the
structured traces proofs. Tidy up a bit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Pointers.ma

    r2185 r2218  
    4242* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
    4343qed.
     44
     45definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?.
     46#x #y @eq_block_elim
     47[ #E destruct /2/
     48| * #NE % #E destruct cases (NE (refl ??))
     49] qed.
    4450
    4551(* This is only required for full 8051 memory spaces.
Note: See TracChangeset for help on using the changeset viewer.