Nuprl Definition : hdf-state-single-val

hdf-state-single-val(X;b) ==
  mk-hdf(Xb,a.let X,b = Xb 
              in let X',fs = X(a) 
                 in let b' ←─ if bag-null(fs) then b else sv-bag-only(fs) b 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 b then t else f fi ,  bfalse: ff,  apply: f 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-state-single-val
hdf-state-single-val(X;b)  ==
    mk-hdf(Xb,a.let  X,b  =  Xb 
                            in  let  X',fs  =  X(a) 
                                  in  let  b'  \mleftarrow{}{}  if  bag-null(fs)  then  b  else  sv-bag-only(fs)  b  fi 
                                        in  <<X',  b'>,  \{b'\}>s.ff;<X,  b>)


Date html generated: 2015_07_17-AM-08_05_53
Last ObjectModification: 2012_11_23-PM-02_09_43

Home Index