Nuprl - Some Definitions

	Some definitions of interest.

increasing	`Def increasing(f;k) == i:(k-1). f(i) < f(i+1)`

	`Thm* k:, f:(k). increasing(f;k) Prop`

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

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

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

	`Thm* Type`

le	`Def AB == B < A`

	`Thm* i,j:. (ij) Prop`

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

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

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

nat_plus	`Def == {i:\| 0 < i }`

	`Thm* Type`

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

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

About: