WhoCites
Definitions
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites compose?
compose
Def (
f
o
g
)(
x
) ==
f
(
g
(
x
))
Thm*
A
,
B
,
C
:Type,
f
:(
B
C
),
g
:(
A
B
).
f
o
g
A
C
Syntax:
f
o
g
has structure:
compose(
f
;
g
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
mb
list
1
Sections
MarkB
generic
Doc
A,B,C:Type, f:(B
C), g:(AB). f o g 
ACA,B,C:Type, f:(BC), g:(AB). f o g AC
