Nuprl Definition : cycle

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

Definitions occuring in Statement :  hd: hd(l) null: null(as) list_ind: list_ind ifthenelse: if then else 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 then else fi  null: null(as) hd: hd(l)
FDL editor aliases :  cycle

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 

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

Theory : list_1

Home Index