WhoCites
Definitions
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites sym?
sym
Def Sym
x
,
y
:
T
.
E
(
x
;
y
) ==
a
,
b
:
T
.
E
(
a
;
b
)
E
(
b
;
a
)
Thm*
T
:Type,
E
:(
T
T
Prop). (Sym
x
,
y
:
T
.
E
(
x
,
y
))
Prop
Syntax:
Sym
x
,
y
:
T
.
E
(
x
;
y
)
has structure:
sym(
T
;
x
,
y
.
E
(
x
;
y
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
mb
list
2
Sections
MarkB
generic
Doc
a,b:T. E(a;b) 
E(b;a)T:Type, E:(T
TProp). (Sym x,y:T. E(x,y)) 
Propa,b:T. E(a;b) E(b;a)T:Type, E:(TTProp). (Sym x,y:T. E(x,y)) Prop
