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`

mapoutl	`Def mapoutl(s) == mapfilter(x.outl(x);x.isl(x);s)`

	`Thm* A,B:Type, s:(A+B) List. mapoutl(s) A List`

isl	`Def isl(x) == InjCase(x; y. true; z. false)`

	`Thm* A,B:Type, x:A+B. isl(x)`

l_member	`Def (x l) == i:. i < \|\|l\|\| & x = l[i] T`

	`Thm* T:Type, x:T, l:T List. (x l) Prop`

outl	`Def outl(x) == InjCase(x; y. y; z. "???")`

	`Thm* A,B:Type, x:A+B. isl(x) outl(x) A`

About: