Nuprl Definition : deq-member
x ∈b L == reduce(λa,b. ((eq a x) ∨bb);ff;L)
Definitions occuring in Statement :
reduce: reduce(f;k;as),
bor: p ∨bq,
bfalse: ff,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
bor: p ∨bq,
apply: f a,
bfalse: ff
FDL editor aliases :
deq-member
Latex:
x \mmember{}\msubb{} L == reduce(\mlambda{}a,b. ((eq a x) \mvee{}\msubb{}b);ff;L)
Date html generated:
2016_05_14-AM-06_30_17
Last ObjectModification:
2015_12_03-PM-02_07_54
Theory : list_0
Home
Index