Definitions
mb
event
system
6
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
decidable
Def
Dec(
P
) ==
P
P
Thm*
A
:Prop. Dec(
A
)
Prop
finite-type
Def
finite-type(
T
) ==
n
:
,
f
:(
n
T
). Surj(
n
;
T
;
f
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
mb
event
system
6
Sections
EventSystems
Doc
P
A:Prop. Dec(A) 
Prop
n:
, f:(n
T). Surj(n; T; f) PA:Prop. Dec(A) Propn:, f:(nT). Surj(n; T; f)
