Nuprl - Some Definitions

select	`Def l[i] == hd(nth_tl(i;l))` `Thm* l:A*, n:. 0n n < \|\|l\|\| l[n] A`
nth_tl	`Def (rec) nth_tl(n;as) == if n z 0 as else nth_tl(n-1;tl(as)) fi` `Thm* as:A, i:. nth_tl(i;as) A`
hd	`Def hd(l) == ListInd(l;"?";h,t,v.h)` `Thm* l:A*. (\|\|l\|\| 1 ) hd(l) A`
tl	`Def tl(l) == ListInd(l;nil;h,t,v.t)` `Thm* l:A. tl(l) A`
le_int	`Def i z j == j < z i` `Thm* i,j:. i z j`
lt_int	`Def i < z j == if i < j true ; false fi` `Thm* i,j:. i < z j`
bnot	`Def b == if b false else true fi` `Thm* b:. b`