Ignore:
Timestamp:
Feb 25, 2013, 11:45:57 AM (7 years ago)
Author:
campbell
Message:

Add observables to FEMeasurable proof; fix silly typo.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2722 r2725  
    400400  ! s0 ← make_initial_state … p;
    401401  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
    402   ! 〈interesting,s2〉 ← exec_steps m ?? (cs_exec … C') g s1;
     402  ! 〈interesting,s2〉 ← exec_steps n ?? (cs_exec … C') g s1;
    403403  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
    404404  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
Note: See TracChangeset for help on using the changeset viewer.