α : Type ?u.63315
β : Type ?u.63318
σ : Type ?u.63321
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
⊢ Nat.Primrec fun n => Nat.succ n
α : Type ?u.63315
β : Type ?u.63318
σ : Type ?u.63321
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
⊢ Primrec₂ Nat.pair
simp [Primrec₂, Primrec]
no goals
α : Type ?u.63315
β : Type ?u.63318
σ : Type ?u.63321
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
⊢ Nat.Primrec fun n => Nat.succ n
constructor