protected in the docs

Stream: general

[Yaël Dillies]

Should we somehow show in the docs whether a declaration is protected?

[Eric Wieser]

and noncomputable while we're playing that game

[Bryan Gin-ge Chen]

I've just created doc-gen#135 and doc-gen#136.

[Yaël Dillies]

Adding them on the same line as lemma/ theorem sounds a bit odd, so I think we could add them as is on the attributes' line.

[Rob Lewis]

It's possible to show if a declaration is protected, but I don't think info about (non)computability is exposed to meta code

[Eric Wieser]

Gabriel Ebner said:

I vote for yellow-black danger stripes, these are surprisingly easy to do in CSS:
noncomputable_bg.png

I assume this formatting was not a serious suggestion; what do we actually want to do in leanprover-community/doc-gen#141?