doc-gen noncomputable

Stream: general

[Yaël Dillies]

doc-gen doesn't show noncomputability anymore. eg docs#Function.extend. This was originally implemented in leanprover-community/doc-gen#141. Can this be restored, @Henrik Böving ?

[Henrik Böving]

a) doc-gen4 does show noncomputability, e.g.: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Complex/Exponential.html#Complex.expMonoidHom
b) Your function is not marked as noncomputable so why do you think it should be by doc-gen? https://github.com/leanprover-community/mathlib4/blob/66e5402e652db5dbe842be209ab0a2adf24b343d//Mathlib/Logic/Function/Basic.lean#L725-L726

[Alex J. Best]

I should fix https://github.com/leanprover/lean4/pull/2610 ...

[Yaël Dillies]

Oh hmm, wrong cause indeed.