Nuprl Definition : es-interface-pair
(X,Y) == eclass-compose2(λxs,ys. if (#(xs) =z 1) ∧b (#(ys) =z 1) then {<only(xs), only(ys)>} else {} fi ;X;Y)
Definitions occuring in Statement :
eclass-compose2: eclass-compose2(f;X;Y)
,
band: p ∧b q
,
ifthenelse: if b then t else f fi
,
eq_int: (i =z j)
,
lambda: λx.A[x]
,
pair: <a, b>
,
natural_number: $n
,
bag-only: only(bs)
,
bag-size: #(bs)
,
single-bag: {x}
,
empty-bag: {}
FDL editor aliases :
es-interface-pair
Latex:
(X,Y) ==
eclass-compose2(\mlambda{}xs,ys. if (\#(xs) =\msubz{} 1) \mwedge{}\msubb{} (\#(ys) =\msubz{} 1) then \{<only(xs), only(ys)>\} else \{\} fi ;X;\000CY)
Date html generated:
2015_07_21-PM-03_44_35
Last ObjectModification:
2012_02_25-PM-02_44_55
Home
Index