Nuprl - Some Definitions

	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`

int_seg	`Def {i..j} == {k:\| i k < j }`

	`Thm* m,n:. {m..n} Type`

length	`Def \|\|as\|\| == Case of as; nil 0 ; a.as' \|\|as'\|\|+1 (recursive)`

	`Thm* A:Type, l:A List. \|\|l\|\|`

	`Thm* \|\|nil\|\|`

nat	`Def == {i:\| 0i }`

	`Thm* Type`

not	`Def A == A False`

	`Thm* A:Prop. (A) Prop`

select	`Def l[i] == hd(nth_tl(i;l))`

	`Thm* A:Type, l:A List, n:. 0n n < \|\|l\|\| l[n] A`

About: