WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc
Who Cites fun
exp?
fun_exp
Def f^n == primrec(n;
x.x;
i,g. f o g)
Thm*
T:Type, n:
, f:(T
T). f^n
T
T
compose
Def
(f o g)(x) == f(g(x))
Thm*
A,B,C:Type, f:(B
C), g:(A
B). f o g
A
C
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:
f^n
has structure:
fun_exp(f; n)
About:
WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc