PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sized
mset
wf5
a
,
k
,
x
:
.
a
{
k
}
{
x
...}
Type
By:
Def of
<nat> {<nat>}
<Nat subtype>
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
a,k,x:
. a {k}
{x...} 
Type a,k,x:. a {k} {x...} Type<nat> {<nat>} <Nat subtype>
