Nuprl Definition : pv11_p1_add_if_new
pv11_p1_add_if_new() == λtest,val,lst. if (∃zzc∈lst.test val zzc)_b then lst else lst @ [val] fi
Definitions occuring in Statement :
bl-exists: (∃x∈L.P[x])_b,
append: as @ bs,
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
pv11_p1_add_if_new
Latex:
pv11\_p1\_add\_if\_new() == \mlambda{}test,val,lst. if (\mexists{}zzc\mmember{}lst.test val zzc)\_b then lst else lst @ [val] fi
Date html generated:
2015_07_23-PM-04_11_25
Last ObjectModification:
2014_11_26-AM-11_23_01
Home
Index