WhoCites
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Associativity of a function
Who Cites is
assoc?
is_assoc
Def is_assoc(
A
;
x
,
z
.
f
(
x
;
z
)) ==
x
,
y
,
z
:
A
.
f
(
x
;
f
(
y
;
z
)) =
f
(
f
(
x
;
y
);
z
)
A
Thm*
A
:Type,
f
:(
A
A
A
). is_assoc(
A
;
x
,
z
.
f
(
x
,
z
))
Prop
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
x,y,z:A. f(x;f(y;z)) = f(f(x;y);z) 
AA:Type, f:(A
AA). is_assoc(A; x,z.f(x,z)) Propx,y,z:A. f(x;f(y;z)) = f(f(x;y);z) AA:Type, f:(AAA). is_assoc(A; x,z.f(x,z)) Prop
