Nuprl Definition : remove-alist
remove-alist(eq;L;x) == rec-case(L) of [] => [] | p::ps => r.let a,v = p in if eq a x then r else [p / r] fi
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
apply: f a,
spread: spread def
Definitions occuring in definition :
list_ind: list_ind,
nil: [],
spread: spread def,
ifthenelse: if b then t else f fi ,
apply: f a,
cons: [a / b]
FDL editor aliases :
remove-alist
Latex:
remove-alist(eq;L;x) ==
rec-case(L) of
[] => []
p::ps =>
r.let a,v = p
in if eq a x then r else [p / r] fi
Date html generated:
2016_05_14-PM-03_22_50
Last ObjectModification:
2015_09_22-PM-05_59_29
Theory : decidable!equality
Home
Index