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