WhoCites
Definitions
mb
tree
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites tree?
tree
Def Tree(
E
) == rec(
T
.tree_con(
E
;
T
))
Thm*
E
:Type. Tree(
E
)
Type
tree_con
Def
tree_con(
E
;
T
) ==
E
+(
T
T
)
Thm*
E
,
T
:Type. tree_con(
E
;
T
)
Type
Syntax:
Tree(
E
)
has structure:
tree(
E
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
mb
tree
Sections
MarkB
generic
Doc
E:Type. Tree(E) 
Type
T)E,T:Type. tree_con(E;T) TypeE:Type. Tree(E) TypeT)E,T:Type. tree_con(E;T) Type
