Nuprl - Some Definitions

	Some definitions of interest.

assert	`Def b == if b True else False fi`

	`Thm* b:. b Prop`

iff	`Def P Q == (P Q) & (P Q)`

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

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`

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

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

About: