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

defined dummy block code equals to 0

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.