Nuprl Definition : hdf-until

hdf-until(X;Y) ==
  mk-hdf(p,a.let X,Y = p 
             in let X',b = X(a) 
                in let Y',c = Y(a) 
                   in <<if bag-null(c) then X' else hdf-halt() fi , Y'>, b>;p.hdf-halted(fst(p));<X, Y>)


Definitions occuring in Statement :  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),  hdf-halt: hdf-halt(),  hdf-halted: hdf-halted(P),  hdf-ap: X(a),  ifthenelse: if b then t else f fi ,  pi1: fst(t),  spread: spread def,  pair: <a, b>,  bag-null: bag-null(bs)
FDL editor aliases :  hdf-until
hdf-until(X;Y)  ==
    mk-hdf(p,a.let  X,Y  =  p 
                          in  let  X',b  =  X(a) 
                                in  let  Y',c  =  Y(a) 
                                      in  <<if  bag-null(c)  then  X'  else  hdf-halt()  fi  ,  Y'>,  b>p.hdf-halted(fst(p));<X
                                                                                                                                                                                                  ,  Y
                                                                                                                                                                                                  >)


Date html generated: 2015_07_17-AM-08_06_06
Last ObjectModification: 2012_11_23-PM-02_09_51

Home Index