Hi, I am trying to write the ackermann function using only primitive recursion using the hott library but it doesn't seem to compute. I realize that use of univalence doesn't compute but I don't think that should change things here unless I am confused

```
Definition ack : nat -> nat -> nat.
Proof.
refine (nat_rec _ _ _).
(* ack 0 n = succ n *)
- exact succ.
- intros m ack_m.
Check nat_rec.
refine (nat_rec _ _ _).
(* ack (succ m) 0 = ack m 1 *)
* exact (ack_m 1%nat).
* intros ack_succ_m_0 ack_succ_m_n.
refine (ack_m _).
exact ack_succ_m_n.
Defined.
Compute ack (succ 0) 0.
```

This gives back:

```
= nat_rec (fun _ : nat => nat -> nat) (fun x : nat => (x.+1)%nat)
(fun (n : nat) (x : (fun _ : nat => nat -> nat) n) =>
nat_rec (fun _ : nat => nat) (x 1%nat)
(fun (n0 : nat) (x0 : (fun _ : nat => nat) n0) => x x0)) 1 0%nat
: nat
```

What does `Print nat_rec`

say?

I'd wonder if it's an axiom for some reason, or if it's marked Opaque (`About nat_rec`

might be better to find that out). In the latter case, vm_compute will help.

@Callan McGill I am unable to reproduce the issue on my end. Univalence will not change anything unless you actually start using it so that's not relevant here. Could you try using `Locate`

on `nat_rec`

just to check we are talking about the same one. I am also assuming you imported `From HoTT Require Import HoTT.`

?

Strange. I get

```
nat_rec
: forall P : nat -> Type0,
P 0%nat ->
(forall n : nat, P n -> P (n.+1)%nat) -> forall n : nat, P n
= 2%nat
: nat
```

Thank you @Paolo Giarrusso ! Once again, I had some bad namespace issue :expressionless:

Last updated: Jun 15 2024 at 08:01 UTC