Nuprl Definition : remove1

as \ a ==  Y (λremove1,as. case as of [] => [] | a'::as' => if a' (=b) a then as' else [a' / (remove1 as')] fi  esac) as


Definitions occuring in Statement :  list_ind: list_ind,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  infix_ap: x f y,  ycomb: Y,  apply: f a,  lambda: λx.A[x],  set_eq: =b
Definitions occuring in definition :  ycomb: Y,  lambda: λx.A[x],  list_ind: list_ind,  nil: [],  ifthenelse: if b then t else f fi ,  infix_ap: x f y,  set_eq: =b,  cons: [a / b],  apply: f a
Latex:
as  \mbackslash{}  a  ==
    Y 
    (\mlambda{}remove1,as.  case  as  of 
                                    []  =>  [] 
                                    a'::as'  =>
                                      if  a'  (=\msubb{})  a  then  as'  else  [a'  /  (remove1  as')]  fi   
                              esac) 
    as


Date html generated: 2016_05_16-AM-07_38_42
Last ObjectModification: 2015_09_23-AM-09_51_36

Theory : list_2


Home Index