Nuprl Definition : aa_data_wrapper_ind
aa_data_wrapper_ind(x;nd,rec1.node[nd; rec1];val.leaf[val]) ==
fix((
aa_data_wrapper_ind,x. case x of inl(x) => node[x; aa_data_wrapper_ind x] | inr(x) => leaf[x])) x
Definitions occuring in Statement :
apply: f a,
lambda: x.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :
aa_data_wrapper_ind
aa\_data\_wrapper\_ind(x;nd,rec1.node[nd; rec1];val.leaf[val]) ==
fix((\mlambda{}aa\_data\_wrapper$_{ind}$,x. case x of inl(x) => node[x; aa\_data\_wrapper\mbackslash{}f\000Cf24_{ind}$ x] | inr(x) => leaf[x])) x
Date html generated:
2013_03_20-AM-11_02_27
Last ObjectModification:
2012_11_27-AM-10_33_07
Home
Index