Nuprl Definition : cycle

cycle(L) ==
  λx.if null(L)
     then x
     else let b = hd(L) in
              rec-case(L) of
              [] => x
              a::as =>
               r.if (x =z a) then if null(as) then b else hd(as) fi  else r fi 
     fi 


Definitions occuring in Statement :  hd: hd(l),  null: null(as),  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  let: let,  lambda: λx.A[x]
Definitions occuring in definition :  lambda: λx.A[x],  let: let,  list_ind: list_ind,  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  null: null(as),  hd: hd(l)
FDL editor aliases :  cycle
Latex:
cycle(L)  ==
    \mlambda{}x.if  null(L)
          then  x
          else  let  b  =  hd(L)  in
                            rec-case(L)  of
                            []  =>  x
                            a::as  =>
                              r.if  (x  =\msubz{}  a)  then  if  null(as)  then  b  else  hd(as)  fi    else  r  fi 
          fi 


Date html generated: 2016_05_14-PM-02_25_33
Last ObjectModification: 2015_09_22-PM-05_55_58

Theory : list_1


Home Index