Linkify builtin types like Sort, Prop, and Pi

[eric-wieser]

It would be good to forward-port the features from:

• feat: add a new page with very basic documentation for Pi/Sort/Type/Prop leanprover-community/doc-gen#172
  Instance lists for builtin types, like we already have for inductive types
• feat: split instance lists between pi and forall and implies and function leanprover-community/doc-gen#173
  Distinguishing between different ways of printing pi types. This probably should adapt to the Lean4 changes around pretty-printing.
• Add support for U+E003 links in Lean 3.49.0 leanprover-community/doc-gen#174
  Linkifying these special types

The PRs above are all centered around this page: https://leanprover-community.github.io/mathlib_docs/foundational_types.html

[hargoniX]

In general it is unclear right now what thing we want to use for documentation that is not directly related to code. Despite building doc-gen4 I have in fact basically no clue about web development at all :D so implementing this type of prose documentation is something I don't want to invest too much time on when I can instead be helping at the code generator front.

There have also been a few people that want to integrate existing documentation tools better with the Lean stuff like LeanInk so maybe this would be the place for documentation like this to live? I'm unsure, where to put what documentation is still an open question :/

[eric-wieser]

The prose itself isn't really what matters here; it's primarily about being able to ask "what instances does mathlib put on pi types", which is very much directly related to code. The components of doing so are roughly:

• finding somewhere to emit "Instances for" for these special builtin types. If you don't want to write any prose, don't bother. Headings alone is enough for now.
• modifying the scraping component to detect typeclasses on pi and Prop etc (you might already have code that does this if you copied it from doc-gen 3)
• Modifying the Lean4 equivalent of pp.links to attach links to these builtin types

[hargoniX]

I do have an implementation in #93 for sort variants. I am not yet sure how to do pi types in the current framework. It might be that this requires a patch similar to the one we had for function applications with constants in the compiler.