Nuprl Definition : ohc_v2_Halt
ohc_v2_Halt() == 
n.slf,m.if (n =
m) then {
} else {} fi @|Loc, ohc_v2_decided'base()|
Definitions occuring in Statement :
ohc_v2_decided'base: ohc_v2_decided'base(),
concat-lifting-loc-1: f@,
simple-loc-comb-1: F|Loc, X|,
eq_int: (i = j),
ifthenelse: if b then t else f fi ,
it: ,
lambda: x.A[x],
single-bag: {x},
empty-bag: {}
FDL editor aliases :
ohc_v2_Halt
ohc\_v2\_Halt() == \mlambda{}n.\mlambda{}slf,m.if (n =\msubz{} m) then \{\mcdot{}\} else \{\} fi @|Loc, ohc\_v2\_decided'base()|
Date html generated:
2012_02_20-PM-05_50_33
Last ObjectModification:
2012_02_17-PM-10_24_44
Home
Index