English
Boolean equality test is primitive recursive for decidable equality types.
Русский
Булевое равенство для типов с разрешимым равенством примитивно вычисимо.
LaTeX
$$$[DecidableEq\\alpha] \\Rightarrow Primrec_2(@BEq.beq\\alpha\\_)$$$
Lean4
/-- To show a function `f : α → ℕ` is primitive recursive, it is enough to show that the function
is bounded by a primitive recursive function and that its graph is primitive recursive -/
theorem of_graph {f : α → ℕ} (h₁ : PrimrecBounded f) (h₂ : PrimrecRel fun a b => f a = b) : Primrec f :=
by
rcases h₁ with ⟨g, pg, hg : ∀ x, f x ≤ g x⟩
refine (nat_findGreatest pg h₂).of_eq fun n => ?_
exact (Nat.findGreatest_spec (P := fun b => f n = b) (hg n) rfl).symm
