0
b else c(n-1,primrec(n-1;b;c)) fi (recursive)
T:Type, n:
, b:T, c:(n
TT). primrec(n;b;c) 
Tj == if i=j true ; false fii,j:
. (i=j) 
| Who Cites primrec? | |
| 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: | primrec(n;b;c) | has structure: | primrec(n; b; c) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |