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
con?
tree_con
Def tree_con(
E
;
T
) ==
E
+(
T
T
)
Thm*
E
,
T
:Type. tree_con(
E
;
T
)
Type
Syntax:
tree_con(
E
;
T
)
has structure:
tree_con(
E
;
T
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
mb
tree
Sections
MarkB
generic
Doc
T)
E,T:Type. tree_con(E;T) 
TypeT)E,T:Type. tree_con(E;T) Type
