Nuprl - Some Definitions

	Some definitions of interest.

arrows	`Def r- > L^k == n:. rn (G:({s:(n List)\| \|\|s\|\| = k & (x,y:\|\|s\|\|. x < y s[x] < s[y]) }\|\|L\|\|). c:\|\|L\|\|, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. \|\|s\|\| = k (x,y:\|\|s\|\|. x < y s[x] < s[y]) G(map(f;s)) = c))`

	`Thm* r:, k:, L: List. r- > L^k Prop`

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

	`Thm* Type`

le	`Def AB == B < A`

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

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

	`Thm* Type`

About: