# Zulip Chat Archive

## 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: Dec 20 2023 at 11:08 UTC