Nuprl Definition : ohc_v1_Halt
ohc_v1_Halt() == 
n.slf,m.if (n =
m) then {
} else {} fi @|Loc, ohc_v1_decided'base()|
Definitions occuring in Statement :
ohc_v1_decided'base: ohc_v1_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_v1_Halt
ohc\_v1\_Halt() == \mlambda{}n.\mlambda{}slf,m.if (n =\msubz{} m) then \{\mcdot{}\} else \{\} fi @|Loc, ohc\_v1\_decided'base()|
Date html generated:
2012_02_20-PM-05_25_56
Last ObjectModification:
2012_02_13-PM-12_58_16
Home
Index