Possible typo in docstring of partial recursive function

Stream: mathlib4

[Ilmārs Cīrulis]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/Partrec.html#Nat.Partrec

Partrec f means that the partial function f : ℕ → ℕ is partially recursive.

There should be f : ℕ →. ℕ instead of f : ℕ → ℕ, right? If that's true, should I make a PR? (I have forgotten how to do that. :sweat_smile:)

[Aaron Liu]

yeah that's probably a typo

[Aaron Liu]

if you want you can make a PR to fix it

[Ilmārs Cīrulis]

Okay, managed to do that (went to branch 'master', made a new branch, then made a commit and pushed it to github, then made a PR on github website). Need to make PRs more often to remember things.

[Ilmārs Cīrulis]

https://github.com/leanprover-community/mathlib4/actions/runs/17718500257/job/50346789123?pr=29655

Lint style (fork) check failed (Error: Process completed with exit code 1.). Something weird happening here.

The same thing happened to me on another PR, too.

[Eric Wieser]

If you look at the error, it looks like the references.bib file is badly-formatted

[Eric Wieser]

Obviously that's not the fault of your PR, and the problem is intead:

• It is wrong on master
• Somehow the tests only detect this on your PR(s)

[Ilmārs Cīrulis]

It happened on the #26129, (https://github.com/leanprover-community/mathlib4/actions/runs/17713685241/job/50335737385?pr=26129), which is mine too.

Maybe that helps.

[Bryan Gin-ge Chen]

If you merge master, this should go away; see: #mathlib4 > CI "lint style" failure @ 💬

[Ilmārs Cīrulis]

Thank you!