Lean4
/-- An alternative inductive definition of `Primrec` which
does not use the pairing function on ℕ, and so has to
work with n-ary functions on ℕ instead of unary functions.
We prove that this is equivalent to the regular notion
in `to_prim` and `of_prim`. -/
inductive Primrec' : ∀ {n}, (List.Vector ℕ n → ℕ) → Prop
| zero : @Primrec' 0 fun _ => 0
| succ : @Primrec' 1 fun v => succ v.head
| get {n} (i : Fin n) : Primrec' fun v => v.get i
|
comp {m n f} (g : Fin n → List.Vector ℕ m → ℕ) :
Primrec' f → (∀ i, Primrec' (g i)) → Primrec' fun a => f (List.Vector.ofFn fun i => g i a)
|
prec {n f g} :
@Primrec' n f →
@Primrec' (n + 2) g →
Primrec' fun v : List.Vector ℕ (n + 1) => v.head.rec (f v.tail) fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)
