Nuprl Definition : insert
insert(a;L) ==  eval x = eval_list(L) in if a ∈b x then x else [a / x] fi 
Definitions occuring in Statement : 
deq-member: x ∈b L
, 
eval_list: eval_list(t)
, 
cons: [a / b]
, 
callbyvalue: callbyvalue, 
ifthenelse: if b then t else f fi 
Definitions occuring in definition : 
callbyvalue: callbyvalue, 
eval_list: eval_list(t)
, 
ifthenelse: if b then t else f fi 
, 
deq-member: x ∈b L
, 
cons: [a / b]
FDL editor aliases : 
insert
Latex:
insert(a;L)  ==    eval  x  =  eval\_list(L)  in  if  a  \mmember{}\msubb{}  x  then  x  else  [a  /  x]  fi 
Date html generated:
2016_05_14-AM-06_52_53
Last ObjectModification:
2015_12_03-PM-02_07_59
Theory : list_0
Home
Index