Changeset 2824 for src/common


Ignore:
Timestamp:
Mar 8, 2013, 5:37:57 PM (7 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/common/StructuredTraces.ma

    r2769 r2824  
    104104#a #H #G [ % | @⊥ /2 by absurd/ ]
    105105qed.
    106 
    107 notation > "Σ_{ ident i ∈ l } f"
    108   with precedence 20
    109   for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
    110 notation < "Σ_{ ident i ∈ l } f"
    111   with precedence 20
    112 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
    113106
    114107definition lift_cost_map_id :
Note: See TracChangeset for help on using the changeset viewer.