Nuprl Definition : aa_ltree
aa_ltree(T) == rec(X.Unit + (val:T 
left_subtree:X X))
Definitions occuring in Statement :
unit: Unit,
rec: rec(x.A[x]),
product: x:A B[x],
union: left + right
FDL editor aliases :
aa_ltree
aa\_ltree(T) == rec(X.Unit + (val:T \mtimes{} left$_{subtree}$:X \mtimes{} X))
Date html generated:
2013_03_20-AM-10_57_31
Last ObjectModification:
2012_11_27-AM-10_32_18
Home
Index