Commit 2025-05-14 17:41 70a5f9ff

View on Github →

style: rename Nat.Partrec.Code.xxx_prim to primrec_xxx (#24811)

Estimated changes

Modified Mathlib/Computability/Halting.lean

Modified Mathlib/Computability/PartrecCode.lean

deleted theorem Nat.Partrec.Code.comp_prim

added theorem Nat.Partrec.Code.computable_recOn

deleted theorem Nat.Partrec.Code.const_prim

deleted theorem Nat.Partrec.Code.curry_prim

deleted theorem Nat.Partrec.Code.evaln_prim

deleted theorem Nat.Partrec.Code.pair_prim

deleted theorem Nat.Partrec.Code.prec_prim

added theorem Nat.Partrec.Code.primrec_const

added theorem Nat.Partrec.Code.primrec_evaln

added theorem Nat.Partrec.Code.primrec_recOn'

added theorem Nat.Partrec.Code.primrec_recOn

added theorem Nat.Partrec.Code.primrec_rfind'

added theorem Nat.Partrec.Code.primrec₂_comp

added theorem Nat.Partrec.Code.primrec₂_curry

added theorem Nat.Partrec.Code.primrec₂_pair

added theorem Nat.Partrec.Code.primrec₂_prec

deleted theorem Nat.Partrec.Code.rec_computable

deleted theorem Nat.Partrec.Code.rec_prim'

deleted theorem Nat.Partrec.Code.rec_prim

deleted theorem Nat.Partrec.Code.rfind_prim