WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc
Who Cites search?
search
Def search(k;P) == primrec(k;0;
i,j. if 0 <
j
j ;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:(
n
T
T). 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:
WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc