Commit 2026-01-19 08:37 dcbaf1aa

View on Github →

refactor: make Nat.Partrec protected (#33891) Nat.Primrec is protected to avoid confusion with Primrec, but Nat.Partrec is not. Furthermore, Nat.Partrec is a definition in recursion theory, so frequently used under open Nat, and as it is an auxiliary definition of Partrec, confusion is particularly problematic. In this PR, we make Nat.Partrec protected.

Estimated changes

modified theorem Nat.Partrec'.of_part
modified theorem Nat.Partrec'.part_iff
modified theorem Nat.Partrec'.part_iff₁
modified theorem Nat.Partrec'.to_part
modified theorem Nat.Partrec.none
modified theorem Nat.Partrec.of_eq
modified theorem Nat.Partrec.of_eq_tot
modified theorem Nat.Partrec.of_primrec
modified theorem Nat.Partrec.ppred
modified theorem Nat.Partrec.prec'
deleted inductive Nat.Partrec