Nuprl Definition : W-select

W-select(w;s)
==r if null(s) then inl w else let a,f = w in case hd(s) a of inl(b) => W-select(f b;tl(s)) | inr(z) => inr z  fi 
W-select(w;s) ==
  fix((λW-select,w,s. if null(s)
                     then inl w
                     else let a,f = w 
                          in case hd(s) a of inl(b) => W-select (f b) tl(s) | inr(z) => inr z 
                     fi )) 
  w 
  s


Definitions occuring in Statement :  hd: hd(l),  null: null(as),  tl: tl(l),  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  null: null(as),  inl: inl x,  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  hd: hd(l),  apply: f a,  tl: tl(l),  inr: inr x 
FDL editor aliases :  W-select
Latex:
W-select(w;s)
==r  if  null(s)
        then  inl  w
        else  let  a,f  =  w 
                  in  case  hd(s)  a  of  inl(b)  =>  W-select(f  b;tl(s))  |  inr(z)  =>  inr  z 
        fi 

Latex:
W-select(w;s)  ==
    fix((\mlambda{}W-select,w,s.  if  null(s)
                                          then  inl  w
                                          else  let  a,f  =  w 
                                                    in  case  hd(s)  a  of  inl(b)  =>  W-select  (f  b)  tl(s)  |  inr(z)  =>  inr  z 
                                          fi  )) 
    w 
    s


Date html generated: 2016_05_15-PM-10_06_32
Last ObjectModification: 2015_09_23-AM-08_22_15

Theory : bar!induction


Home Index