Open Command-Master opened 2 months ago
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.
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.