Show instances available for a given type

[eric-wieser]

I have no idea what I'm doing with this meta code, so it's entirely plausible there is a much better way to do this.

The heuristics for choosing what to display are overly generous, mainly because I don't know how to work with binders effectively in meta code. Ideally instances about list.lex wouldn't show up under the list of instances for list, but that would need something that notices when type arguments to typeclasses are used as indices to later type arguments to typeclasses.

Either way, it seems to be collecting moderately helpful information.

We might want a special page that lists instances on pi, Type, Prop, and Sort; this PR collects the data for instances on those types, but doesn't attempt to render it anywhere

Zulip thread

[eric-wieser]

deploy

[github-actions[bot]]

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

[eric-wieser]

Some examples:

alg_equiv	monoid_algebra	nat
		...

Things like nat and list have a fair bit of junk in their list that might be less interesting.

[ericrbg]

i'd be very happy to see this!

[gebner]

deploy

[gebner]

Deploy failed because this branch doesn't have 330e01df63a71a645abe664727584fb3932326d8 yet.

[gebner]

deploy

[github-actions[bot]]

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

[eric-wieser]

deploy

[github-actions[bot]]

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

[eric-wieser]

deploy

[github-actions[bot]]

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

[gebner]

Thanks!