n:
, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))
0
b else c(n-1,primrec(n-1;b;c)) fi (recursive)
is mentioned by
| Thm* n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n)) | [primrec_list_accum] |
In prior sections: mb nat mb list 1
Try larger context:
Graphs