Nuprl Definition : mk-set-nat-missing
mk-set-nat-missing() ==
mk-set(ℕ;nat-missing-type();λi,s. member-nat-missing(i;s);empty-nat-missing();λs.isEmpty-nat-missing(s);
λi.singleton-nat-missing(i);λi,s. add-nat-missing(i;s);λs1,s2. union-nat-missing(s1;s2);λi,s. remove-nat-missin\000Cg(i;s))
Definitions occuring in Statement :
remove-nat-missing: remove-nat-missing(i;s),
union-nat-missing: union-nat-missing(s1;s2),
add-nat-missing: add-nat-missing(i;s),
singleton-nat-missing: singleton-nat-missing(i),
isEmpty-nat-missing: isEmpty-nat-missing(s),
empty-nat-missing: empty-nat-missing(),
member-nat-missing: member-nat-missing(i;s),
nat-missing-type: nat-missing-type(),
mk-set: mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove),
nat: ℕ,
lambda: λx.A[x]
FDL editor aliases :
mk-set-nat-missing
Latex:
mk-set-nat-missing() ==
mk-set(\mBbbN{};nat-missing-type();\mlambda{}i,s. member-nat-missing(i;s);empty-nat-missing();
\mlambda{}s.isEmpty-nat-missing(s);\mlambda{}i.singleton-nat-missing(i);\mlambda{}i,s. add-nat-missing(i;s);
\mlambda{}s1,s2. union-nat-missing(s1;s2);\mlambda{}i,s. remove-nat-missing(i;s))
Date html generated:
2016_05_17-PM-01_46_28
Last ObjectModification:
2013_04_02-AM-00_32_10
Theory : datatype-signatures
Home
Index