Nuprl Definition : es-interface-part
(X|g=i) == λeo,e. let b = X eo e in if (#(b) =z 1) then if g e = i then b else {} fi else {} fi
Definitions occuring in Statement :
eq_id: a = b
,
ifthenelse: if b then t else f fi
,
eq_int: (i =z j)
,
let: let,
apply: f a
,
lambda: λx.A[x]
,
natural_number: $n
,
bag-size: #(bs)
,
empty-bag: {}
FDL editor aliases :
es-interface-part
Latex:
(X|g=i) == \mlambda{}eo,e. let b = X eo e in if (\#(b) =\msubz{} 1) then if g e = i then b else \{\} fi else \{\} fi
Date html generated:
2015_07_20-PM-03_36_39
Last ObjectModification:
2012_02_25-PM-01_50_44
Home
Index