Changeset 2824 for src/utilities


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/utilities/extranat.ma

    r2767 r2824  
    167167qed.
    168168
     169(* notation for sum *)
     170notation > "Σ_{ ident i ∈ l } f"
     171  with precedence 20
     172  for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
     173notation < "hvbox(Σ_{ ident i break ∈ l } break f)"
     174  with precedence 20
     175for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
     176
Note: See TracChangeset for help on using the changeset viewer.