Lean 4 docs don't always label noncomputable defs

Stream: lean4

[Matt Diamond]

Not sure if this is a known issue but there are cases where the Lean 4 docs don't mark noncomputable defs as such. One example is docs#Cardinal.aleph. I'm guessing that the doc generator isn't picking up on the noncomputable section notation at the top of the file.

[Matt Diamond]

I assume the docs are generated via https://github.com/leanprover/doc-gen4, so perhaps I'll just open an issue there.

[Eric Wieser]

I think the problem here is that while not having executable code, these are genuinely not noncomputable

[Eric Wieser]

...and the fact these two things are different feels like a (low priority) misfeature in core, not in the docs

[Alex J. Best]

Yeah this is #2610 again, which I haven't had time to fix yet

[Eric Wieser]

lean4#2610?