noncomputable section isn't shown anywhere
Command-Master opened this issue · 2 comments
When a definition appears in a noncomputable section, while the definition is actually noncomputable, there is no indication given for that anywhere in the docs, and it appears just like a computable definition.
doc-gen asks the Environment whether something is non computable by calling this function: https://leanprover-community.github.io/mathlib4_docs/Lean/Compiler/NoncomputableAttr.html#Lean.isNoncomputable If noncomputable section does not hook itself up with this there is not much I can do, unless it registers the noncomputability in another part of the Environment.
From what I can see noncomputable section affects Lean.Elab.Command.Scope.isNoncomputable, but it does need to attempt compilation for everything before it can decide if it should be made noncomputable, so I'm not sure how this can be detected.