## Stream: new members

### Topic: more primrec examples?

#### Jia Ming (Dec 10 2020 at 08:29):

Hello, I'm exploring the computability folder right now and I absolutely LOVE it. Would mathlib welcome additional theorems like primrec nat.fact or primrec_pred nat.prime? The first one is a short proof that makes use of prec1 (not used anywhere else) and I don't know how the 2nd one will turn out yet. I could look and see where other typical textbook examples could fit in to mathlib nicely.

namespace nat
namespace primrec
-- proof that taking factorials is primitive recursive
theorem fact : primrec fact :=
(prec1 1 (mul'.comp (pair right (succ.comp left)))).of_eq \$
λ n, by simp; induction n; simp [*, mul_comm]

end primrec
end nat


Also, I noticed some omissions like primrec.nat_pow despite mathlib having nat.primrec.pow, while add, sub and mul are all synced, which to me looks like missing API.. Should I make a PR including these additions (if they are welcome)?

#### Mario Carneiro (Dec 10 2020 at 10:49):

Sure! The theorems that are in there are mostly those that I needed to build up to higher level theorems, but of course there are many functions in mathlib and most of the computable functions are primrec.

#### Jia Ming (Dec 10 2020 at 12:22):

Yay! awesome

Last updated: May 15 2021 at 00:39 UTC