x.x;i,g. f o g)
T:Type, n:
, f:(T
T). f^n 
TTA,B,C:Type, f:(BC), g:(AB). f o g AC
0
b else c(n-1,primrec(n-1;b;c)) fi (recursive)T:Type, n:, b:T, c:(nTT). primrec(n;b;c) Tj == if i=j true ; false fii,j:
. (i=j) 
| Who Cites fun exp? | |
| fun_exp | Def f^n == primrec(n;x.x;i,g. f o g) |
| Thm* T:Type, n:, f:(TT). f^n TT | |
| compose | Def (f o g)(x) == f(g(x)) |
| Thm* A,B,C:Type, f:(BC), g:(AB). f o g AC | |
| 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: | f^n | has structure: | fun_exp(f; n) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |