Changeset 227


Ignore:
Timestamp:
Nov 9, 2010, 12:52:38 PM (9 years ago)
Author:
campbell
Message:

Update notation in an example.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/test/io2.c.ma

    r124 r227  
    2929(* ndefinition works fine for this, whereas nletin during proof seems to blow up. *)
    3030ndefinition s ≝ (
    31  ! s0 ← make_initial_state myprog;:
    32  ! 〈t,s〉 ← exec_steps 13 (globalenv Genv ?? myprog) s0;:
     31 ! s0 ← make_initial_state myprog;
     32 ! 〈t,s〉 ← exec_steps 13 (globalenv Genv ?? myprog) s0;
    3333   ret ? s).
    3434
Note: See TracChangeset for help on using the changeset viewer.