how to document `partial` restriction?

Stream: lean4

[Arthur Paulino]

Leo explained to me that partial cannot be used on functions whose return type might be empty. I tried to PR an explanation with the examples that he showed me but a test is capturing the fact that I (intentionally) introduced code that doesn't compile.

This is the PR

My question is: how to explain it without showing code that doesn't compile?

[Sebastian Ullrich]

You can use

```lean,ignore

code blocks for that