Nuprl - Definition Cascade for search

	Who Cites search?

search	`Def search(k;P) == primrec(k;0;i,j. if 0 < jj ;P(i)i+1 else 0 fi)`

	`Thm* k:, P:(k). search(k;P) (k+1)`

lt_int	`Def i < j == if i < j true ; false fi`

	`Thm* i,j:. (i < j)`

primrec	`Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi (recursive)`

	`Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c) T`

eq_int	`Def i=j == if i=j true ; false fi`

	`Thm* i,j:. (i=j)`

Syntax: search(k;P) has structure: search(k; P)

About: