Nuprl Definition : list-index

list-index(d;L;x) ==
  rec-case(L) of
  [] => inr ⋅ 
  z::L' => of inl(n) => inl (n 1) inr(a) => if eqof(d) then inl else fi 

Definitions occuring in Statement :  list_ind: list_ind eqof: eqof(d) ifthenelse: if then else fi  it: apply: a decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x add: m natural_number: $n
Definitions occuring in definition :  list_ind: list_ind inr: inr  it: decide: case of inl(x) => s[x] inr(y) => t[y] add: m ifthenelse: if then else fi  apply: a eqof: eqof(d) inl: inl x natural_number: $n
FDL editor aliases :  list-index

list-index(d;L;x)  ==
    rec-case(L)  of
    []  =>  inr  \mcdot{} 
    z::L'  =>  r  of  inl(n)  =>  inl  (n  +  1)  |  inr(a)  =>  if  eqof(d)  z  x  then  inl  0  else  r  fi 

Date html generated: 2016_05_14-PM-03_30_21
Last ObjectModification: 2015_09_22-PM-05_59_51

Theory : decidable!equality

Home Index