Definitions
mb
event
system
1
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
append
Def
as
@
bs
== Case of
as
; nil
bs
;
a
.
as'
[
a
/ (
as'
@
bs
)] (recursive)
Thm*
T
:Type,
as
,
bs
:
T
List. (
as
@
bs
)
T
List
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
1
Sections
EventSystems
Doc
bs ; a.as' [a / (as' @ bs)] (recursive)
T:Type, as,bs:T List. (as @ bs) 
T List Type bs ; a.as' [a / (as' @ bs)] (recursive)T:Type, as,bs:T List. (as @ bs) T List Type
