this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => Part.bind ↑(decode n₁) fun a => Part.map encode (f a)
⊢ Partrec' f
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
⊢ Partrec' f
let g := fun n₁ =>
  (Part.ofOption (decode (α := Vector ℕ n) n₁)).bind (fun a => Part.map encode (f a))
no goals
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => Part.bind ↑(decode n₁) fun a => Part.map encode (f a)
⊢ Partrec' f
exact
  (comp₁ g (this g hf) (prim Nat.Primrec'.encode)).of_eq fun i => by
    dsimp only; simp [encodek, Part.map_id']
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => Part.bind ↑(decode n₁) fun a => Part.map encode (f a)
i : Vector ℕ n
⊢ (Part.bind ↑(decode (encode i)) fun a => Part.map encode (f a)) = f i
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => Part.bind ↑(decode n₁) fun a => Part.map encode (f a)
i : Vector ℕ n
⊢ g (encode i) = f i
dsimp only
no goals
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => Part.bind ↑(decode n₁) fun a => Part.map encode (f a)
i : Vector ℕ n
⊢ (Part.bind ↑(decode (encode i)) fun a => Part.map encode (f a)) = f i
simp [encodek, Part.map_id']
case intro
c : Code
hf : Partrec (eval c)
⊢ Partrec' fun v => eval c (Vector.head v)
f : ℕ →. ℕ
hf : Partrec f
⊢ Partrec' fun v => f (Vector.head v)
obtain ⟨c, rfl⟩ := exists_code.1 hf
no goals
case intro
c : Code
hf : Partrec (eval c)
⊢ Partrec' fun v => eval c (Vector.head v)
simpa [eval_eq_rfindOpt] using
  rfindOpt <|
    of_prim <|
      Primrec.encode_iff.2 <|
        evaln_prim.comp <|
          (Primrec.vector_head.pair (_root_.Primrec.const c)).pair <|
            Primrec.vector_head.comp Primrec.vector_tail