Nuprl Definition : set-add
a + b == let T,f = a in let S,g = b in <T + S, λx.case x of inl(t) => f t | inr(s) => g s>
Definitions occuring in Statement :
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
union: left + right
Definitions occuring in definition :
apply: f a,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
lambda: λx.A[x],
union: left + right,
pair: <a, b>,
spread: spread def
FDL editor aliases :
set-add
Latex:
a + b == let T,f = a in let S,g = b in <T + S, \mlambda{}x.case x of inl(t) => f t | inr(s) => g s>
Date html generated:
2018_07_29-AM-09_59_51
Last ObjectModification:
2018_07_18-AM-11_28_19
Theory : constructive!set!theory
Home
Index