Changeset 2592 for src/joint


Ignore:
Timestamp:
Jan 29, 2013, 11:20:53 AM (7 years ago)
Author:
piccolo
Message:

main lemma of ERTLptr in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2590 r2592  
    7777  mk_program_counter «mk_block Code (-1), refl …» one.
    7878
    79 definition null_pc : program_counter ≝
    80     mk_program_counter «mk_block Code OZ, refl …» one.
     79definition null_pc : Pos →  program_counter ≝ λpos.
     80    mk_program_counter «mk_block Code OZ, refl …» pos.
    8181
    8282definition set_m: ∀p. bemem → state p → state p ≝
Note: See TracChangeset for help on using the changeset viewer.