Nuprl Definition : int-list-index

int-list-index(L;x) ==  rec-case(L) of [] => 0 | a::as => r.if (a =z x) then 0 else r + 1 fi 


Definitions occuring in Statement :  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  add: n + m,  natural_number: $n
Definitions occuring in definition :  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  add: n + m,  natural_number: $n
FDL editor aliases :  int-list-index
Latex:
int-list-index(L;x)  ==    rec-case(L)  of  []  =>  0  |  a::as  =>  r.if  (a  =\msubz{}  x)  then  0  else  r  +  1  fi 


Date html generated: 2016_05_15-PM-04_23_47
Last ObjectModification: 2015_09_23-AM-07_48_15

Theory : general


Home Index