Changeset 2641 for src


Ignore:
Timestamp:
Feb 7, 2013, 3:15:56 PM (7 years ago)
Author:
piccolo
Message:

defined dummy block code equals to 0

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Pointers.ma

    r2608 r2641  
    2727definition block_region : block → region ≝
    2828  λb.
    29   if Zltb (block_id b) OZ then
     29  if Zleb (block_id b) OZ then
    3030    Code
    3131  else
    3232    XData.
     33
     34definition dummy_block_code : block ≝
     35mk_block OZ.
    3336
    3437definition eq_block ≝
  • src/joint/joint_semantics.ma

    r2638 r2641  
    7878
    7979definition null_pc : Pos →  program_counter ≝ λpos.
    80     mk_program_counter «mk_block ?, ?» pos.
    81 cases daemon qed.
     80    mk_program_counter «dummy_block_code, refl …» pos.
    8281
    8382definition set_m: ∀p. bemem → state p → state p ≝
Note: See TracChangeset for help on using the changeset viewer.