Nuprl Definition : sub-es-pred
sub-es-pred(es;dom;e) ==
fix((λsub-es-pred,e. if first(e) then inr ⋅ if dom pred(e) then inl pred(e) else sub-es-pred pred(e) fi )) e
Definitions occuring in Statement :
es-first: first(e),
es-pred: pred(e),
ifthenelse: if b then t else f fi ,
it: ⋅,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
inr: inr x ,
inl: inl x
FDL editor aliases :
sub-es-pred
sub-es-pred
sub-es-pred(es;dom;e) ==
fix((\mlambda{}sub-es-pred,e. if first(e) then inr \mcdot{}
if dom pred(e) then inl pred(e)
else sub-es-pred pred(e)
fi ))
e
Date html generated:
2015_07_17-AM-09_05_47
Last ObjectModification:
2013_03_25-PM-01_43_44
Home
Index