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.
selectDef l[i] == hd(nth_tl(i;l))
Thm* A:Type, l:A List, n:. 0n  n<||l||  l[n A
hdDef hd(l) == Case of l; nil  "?" ; h.t  h
Thm* A:Type, l:A List. ||l|| hd(l A
int_segDef {i..j} == {k:i  k < j }
Thm* m,n:. {m..n Type
lengthDef ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
Thm* A:Type, l:A List. ||l||  
Thm* ||nil||  
mapDef map(f;as) == Case of as; nil  nil ; a.as'  [(f(a)) / map(f;as')]
Def (recursive)
Thm* A,B:Type, f:(AB), l:A List. map(f;l B List
Thm* A,B:Type, f:(AB), l:A List. map(f;l B List
notDef A == A  False
Thm* A:Prop. (A Prop
nth_tlDef nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi  (recursive)
Thm* A:Type, as:A List, i:. nth_tl(i;as A List
topDef Top == Void given Void
Thm* Top  Type

About:
listconsnillist_ind
ifthenelsevoidintnatural_numberaddsubtractless_thantoken
setisectapplyfunctionrecursive_def_notice
universemembertoppropimpliesfalseall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb event system 1 Sections EventSystems Doc