Definitions
mb
event
system
4
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
deq
Def
EqDecider(
T
) ==
eq
:
T
T
x
,
y
:
T
.
x
=
y
(
eq
(
x
,
y
))
Thm*
T
:Type. EqDecider(
T
)
Type
eqof
Def
eqof(
d
) == 1of(
d
)
Thm*
T
:Type,
d
:EqDecider(
T
). eqof(
d
)
T
T
top
Def
Top == Void given Void
Thm*
Top
Type
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
event
system
4
Sections
EventSystems
Doc
T
x,y:T. x = y 
(eq(x,y))T:Type. EqDecider(T) 
TypeT:Type, d:EqDecider(T). eqof(d) TT TypeTx,y:T. x = y (eq(x,y))T:Type. EqDecider(T) TypeT:Type, d:EqDecider(T). eqof(d) TT Type
