feat: partial_fixpoint

[nomeata]

The manual section to go with leanprover/lean4#6355.

[nomeata]

Direct link to new section: https://draft-pr-253--lean-reference-manual-review.netlify.app/Recursive-Definitions/Partial-Fixpoint-Recursion/#partial-fixpoint

[nomeata]

Ok, marking this as ready for review for now, and will try to keep my hands away from it.

I’ll merge the feature to Lean4 master next, but presumably this PR should not enter main until the feature is in a pre-release? So there is no rush with getting this into shape.

I left some todo notes where my Verso-skills failed me, but none are critical, they are all just nice-to haves.

[github-actions]

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 8b46c56.