leanprover-community / doc-gen

Generate HTML documentation for mathlib and Lean

https://leanprover-community.github.io/mathlib_docs/

Apache License 2.0

21 stars 20 forks source link

Show `noncomputable` in the docs #141

Closed eric-wieser closed 2 years ago

eric-wieser commented 2 years ago

Closes #136. Hovering over the word noncomputable gives a brief summary of why definitions are noncomputable.

If the deployment is not stale, https://leanprover-community.github.io/mathlib_docs_demo/data/real/ereal.html is a good place to see this in action.

This also adds the css classes meta and noncomputable to declarations, in case we decide we want to style these a certain way in future.

Some discussion about styling on Zulip here; for now, we add no special styling and only insert the word noncomputable before associated definitions and instances.

eric-wieser commented 2 years ago

deploy

github-actions[bot] commented 2 years ago

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

eric-wieser commented 2 years ago

Oops, now this only shows the noncomputable declarations!

eric-wieser commented 2 years ago

deploy

github-actions[bot] commented 2 years ago

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

eric-wieser commented 2 years ago

deploy

github-actions[bot] commented 2 years ago

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

eric-wieser commented 2 years ago

deploy

github-actions[bot] commented 2 years ago

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!