Nuprl Definition : list_ind_reverse

list_ind_reverse(L;nilcase;R) ==
  fix((λF,l. if (||l|| =z 0) then nilcase else R (F firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l) fi )) L


Definitions occuring in Statement :  firstn: firstn(n;as),  last: last(L),  length: ||as||,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  firstn: firstn(n;as),  subtract: n - m,  length: ||as||,  natural_number: $n,  last: last(L)
FDL editor aliases :  list_ind_reverse
Latex:
list\_ind\_reverse(L;nilcase;R)  ==
    fix((\mlambda{}F,l.  if  (||l||  =\msubz{}  0)
                        then  nilcase
                        else  R  (F  firstn(||l||  -  1;l))  firstn(||l||  -  1;l)  last(l)
                        fi  )) 
    L


Date html generated: 2016_05_14-PM-02_59_16
Last ObjectModification: 2015_09_22-PM-05_58_10

Theory : list_1


Home Index