Nuprl Definition : list-index

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

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

Latex:
list-index(d;L;x) == rec-case(L) of [] => inr \mcdot{} z::L' => r.case 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