mb tree Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Case tree_leaf(x) => body(xcont(x1,z)
Def == InjCase(x1x2body(x2); _cont(z,z))

is mentioned by

Def leaf_value(t) == Case(t) Case tree_leaf(l) => l Default => True[leaf_value]
Def is_leaf(t) == Case(t) Case tree_leaf(l) => true Default => false[is_leaf]
Def t_iterate(l;n;t)
Def == Case(t)
Def == Case x;y =>
Def == Casen(t_iterate(l;n;x),t_iterate(l;n;y))
Def == Case tree_leaf(x) =>
Def == Casel(x)
Def == Default => True
Def (recursive)
[t_iterate]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb tree Sections MarkB generic Doc