Nuprl Definition : hdf-state1-single-val

hdf-state1-single-val(f;X;b) ==
  mk-hdf(Xb,a.let X,b Xb 
              in let X',xs X(a) 
                 in let b' ⟵ if bag-null(xs) then else sv-bag-only(xs) fi 
                    in <<X', b'>{b'}>;s.ff;<X, b>)



Definitions occuring in Statement :  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) hdf-ap: X(a) callbyvalueall: callbyvalueall ifthenelse: if then else fi  bfalse: ff apply: a spread: spread def pair: <a, b> sv-bag-only: sv-bag-only(b) bag-null: bag-null(bs) single-bag: {x}
FDL editor aliases :  hdf-state1-single-val

Latex:
hdf-state1-single-val(f;X;b)  ==
    mk-hdf(Xb,a.let  X,b  =  Xb 
                            in  let  X',xs  =  X(a) 
                                  in  let  b'  \mleftarrow{}{}  if  bag-null(xs)  then  b  else  f  sv-bag-only(xs)  b  fi 
                                        in  <<X',  b'>,  \{b'\}>s.ff;<X,  b>)



Date html generated: 2016_05_16-AM-10_40_34
Last ObjectModification: 2012_11_23-PM-02_09_44

Theory : halting!dataflow


Home Index