Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
is_ident
Def
is_ident(
A
;
f
;
u
) ==
x
:
A
.
f
(
u
,
x
) =
x
&
f
(
x
,
u
) =
x
Thm*
f
:(
A
A
A
),
u
:
A
. is_ident(
A
;
f
;
u
)
Prop
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
x:A. f(u,x) = x & f(x,u) = xf:(A
AA), u:A. is_ident(A; f; u) 
Prop
== {i:
| 0
i } Typex:A. f(u,x) = x & f(x,u) = xf:(AAA), u:A. is_ident(A; f; u) Prop == {i:| 0i } Type
