Definitions
mb
tree
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
subtype
Def
S
T
==
x
:
S
.
x
T
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
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
tree
Sections
MarkB
generic
Doc
T == 
x:S. x 
TE:Type. Tree(E) Type
T)E,T:Type. tree_con(E;T) Type T == x:S. x TE:Type. Tree(E) TypeT)E,T:Type. tree_con(E;T) Type
