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
es-init(es;e) == final-iterate(\mlambda{}e.if first(e) then ff else inl pred(e) fi ;e)
Date html generated:
2015_07_17-AM-08_44_59
Last ObjectModification:
2013_03_25-PM-01_49_05
Home
Index