Nuprl Definition : list_ind

rec-case(L) of
[] => nilcase
h::t =>
 r.F[h; t; r] ==
  fix((λlist_ind,L. eval v = L in
                    if v is a pair then let h,t = v 
                                        in F[h; t; list_ind t] otherwise if v = Ax then nilcase otherwise ⊥)) 
  L


Definitions occuring in Statement :  bottom: ⊥,  callbyvalue: callbyvalue,  ispair: if z is a pair then a otherwise b,  isaxiom: if z = Ax then a otherwise b,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  callbyvalue: callbyvalue,  ispair: if z is a pair then a otherwise b,  spread: spread def,  apply: f a,  isaxiom: if z = Ax then a otherwise b,  bottom: ⊥
FDL editor aliases :  list_ind
Latex:
rec-case(L)  of
[]  =>  nilcase
h::t  =>
  r.F[h;  t;  r]  ==
    fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                      if  v  is  a  pair  then  let  h,t  =  v 
                                                                              in  F[h;  t;  list$_{ind}$  t]
                                      otherwise  if  v  =  Ax  then  nilcase  otherwise  \mbot{})) 
    L


Date html generated: 2016_05_14-AM-06_26_38
Last ObjectModification: 2015_12_03-PM-02_04_44

Theory : list_0


Home Index