Nuprl - Some Definitions

multi_action	`Def multi_action(l; s; ASet) == if null(l) s else ASet.act(hd(rev(l)),multi_action(ASet.act; rev(tl(rev(l))); s)) fi (recursive)`
reverse	`Def rev(as) == Case of as; nil nil ; a.as' rev(as') @ [a] (recursive)` `Thm* T:Type, as:T. rev(as) T`
tl	`Def tl(l) == Case of l; nil nil ; h.t t` `Thm* A:Type, l:A. tl(l) A`
aset_act	`Def a.act == 2of(a)` `Thm* T:Type, a:ActionSet(T). a.act Ta.cara.car`
hd	`Def hd(l) == Case of l; nil "?" ; h.t h` `Thm* A:Type, l:A*. \|\|l\|\|1 hd(l) A`
null	`Def null(as) == Case of as; nil true ; a.as' false Thm* T:Type, as:T. null(as)` `Thm null(nil)`
append	`Def as @ bs == Case of as; nil bs ; a.as' a.(as' @ bs) (recursive)` `Thm* T:Type, as,bs:T. (as @ bs) T`
pi2	`Def 2of(t) == t.2` `Thm* A:Type, B:(AType), p:a:AB(a). 2of(p) B(1of(p))`

About: