Changeset 2824 for src/joint/Joint.ma


Ignore:
Timestamp:
Mar 8, 2013, 5:37:57 PM (8 years ago)
Author:
tranquil
Message:
  • moved sum on lists notation to extranat
  • used sum on lists to define portion of stack occupied by globals
  • corrected probable bug in joint semantics, where initial state would not move stack pointer past globals before setting up main
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2823 r2824  
    603603   [ ] (prog_funct ?? pr).
    604604
     605definition globals_stacksize : ∀p.joint_program p → nat ≝
     606 λpars,p.
     607 Σ_{entry ∈ prog_vars … p}(\snd entry).
     608
Note: See TracChangeset for help on using the changeset viewer.