PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
is
list
mem
split
A
:Type,
x
,
a
:
A
,
ys
:
A
List. (
x
a
.
ys
)
x
=
a
(
x
ys
)
By:
Compute
x
a
.
ys
*
a
=
x
A
(
x
ys
)
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:Type, x,a:A, ys:A List. (x 
a.ys) 
x = a 
(x ys) A:Type, x,a:A, ys:A List. (x a.ys) x = a (x ys)
x a.ys
* a = x A (x ys)
