mathlib
mathlib copied to clipboard
chore(computability/primrec): remove nolints
I'm not sure if it's a good idea to mark new things as reducible, especially if the only benefit is some golf - sometimes reducible
is regarded as code smell; so I'm very hesitant about this change being in a chore nolint PR.
No idea what I was thinking with the reducible
tags, they've been reverted.
Thanks!
bors merge
Pull request successfully merged into master.
Build succeeded: