doc-gen#163 - reverse instance lookup

Stream: PR reviews

[Eric Wieser]

Over at doc-gen#163, I've tried a rough attempt at showing what instances are available for a given type. See the PR comments for some screenshots.

[Eric Wieser]

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

[Kevin Buzzard]

Oh nice!

[Eric Wieser]

Ideally instances about list.lex wouldn't show up under the list of instances for list

[Eric Wieser]

But that would need something that notices when type arguments to typeclasses are used as indices to later type arguments to typeclasses

[Eric Wieser]

Unrelatedly, we might want a special page that lists instances on pi, Type, Prop, and Sort

[Eric Wieser]

Generating that page would be easy, it's just a question of how to present it and where to put it

[Eric Wieser]

Any more thoughts on this?

[Jireh Loreaux]

ummm... I love it? :heart:

[Eric Wieser]

For bikeshedding: Any better suggestions than "Available typeclasses" for the heading?

[Eric Rodriguez]

Instances?

[Eric Rodriguez]

or related instances?

[Yaël Dillies]

"Fulfilled instances"?

[Eric Wieser]

"Instances" is the heading we use under class for the things that are instances _of_ it

[Eric Wieser]

/poll What should the heading be called

[Eric Wieser]

In hindsight typeclass was a bad word to use, since it lists the instances not their types (classes)

[Eric Wieser]

I've gone with "Available instances"

[Eric Wieser]

This ended up changing to "instances for foo" in review, but is now merged. See docs#nat and docs#lp for examples

[Eric Wieser]

Eric Wieser said:

Unrelatedly, we might want a special page that lists instances on pi, Type, Prop, and Sort

(done, see https://leanprover-community.github.io/mathlib_docs_demo/foundational_types.html#pi-types-code%CF%80-a--%CE%B1-%CE%B2-acode)

[Kevin Buzzard]

Are there any instances on Type which aren't also instances on Type u?