Nuprl Definition : es-init
es-init(es;e) == final-iterate(λe.if first(e) then ff else inl pred(e) fi ;e)
Definitions occuring in Statement :
es-first: first(e),
es-pred: pred(e),
ifthenelse: if b then t else f fi ,
bfalse: ff,
lambda: λx.A[x],
inl: inl x,
final-iterate: final-iterate(f;x)
FDL editor aliases :
es-init
es-init
Latex:
es-init(es;e) == final-iterate(\mlambda{}e.if first(e) then ff else inl pred(e) fi ;e)
Date html generated:
2016_05_16-AM-09_39_10
Last ObjectModification:
2013_03_25-PM-01_49_05
Theory : new!event-ordering
Home
Index