Nuprl Definition : lookup

as[k] ==  Y (λlookup,as. case as of [] => z | b::bs => let bk,bv = b in if bk (=b) k then bv else lookup bs fi  esac) as


Definitions occuring in Statement :  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  infix_ap: x f y,  ycomb: Y,  apply: f a,  lambda: λx.A[x],  spread: spread def,  set_eq: =b
Definitions occuring in definition :  ycomb: Y,  lambda: λx.A[x],  list_ind: list_ind,  spread: spread def,  ifthenelse: if b then t else f fi ,  infix_ap: x f y,  set_eq: =b,  apply: f a
Latex:
as[k]  ==
    Y 
    (\mlambda{}lookup,as.  case  as  of 
                                  []  =>  z 
                                  b::bs  =>
                                    let  bk,bv  =  b 
                                    in  if  bk  (=\msubb{})  k  then  bv  else  lookup  bs  fi   
                            esac) 
    as


Date html generated: 2016_05_16-AM-08_16_35
Last ObjectModification: 2015_09_23-AM-09_52_51

Theory : polynom_2


Home Index