Nuprl Definition : hdf-cbva-simple
hdf-cbva-simple(L;m) == fix((λmk-hdf.(inl (λa.simple-cbva-seq(L[a];λout.<mk-hdf, out>;m)))))
Definitions occuring in Statement :
so_apply: x[s]
,
fix: fix(F)
,
lambda: λx.A[x]
,
pair: <a, b>
,
inl: inl x
,
simple-cbva-seq: simple-cbva-seq(L;F;m)
FDL editor aliases :
hdf-cbva-simple
hdf-cbva-simple(L;m) == fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.simple-cbva-seq(L[a];\mlambda{}out.<mk-hdf, out>m)))))
Date html generated:
2015_07_17-AM-08_08_05
Last ObjectModification:
2012_11_23-PM-02_10_12
Home
Index