Link to files

Stream: Is there code for X?

[Yaël Dillies]

What is the correct way to link to mathlib files in the docs? So far the only examples I've found were mine and linked to data.list.defs by doing

[`data.list.defs`](./defs)

However, I don't know how to refer to order.filter.n_ary from data.set.basic, for example. Would it be

[`order.filter.n_ary`](../../order/filter/n_ary)

[Eric Wieser]

That ought to work

[Eric Wieser]

A better option would be to teach doc-gen a syntax for file links

[Eric Wieser]

Something as simple as [import:order.filter][] could probably be made to work

[Eric Wieser]

Something as simple as [import:order.filter][] could probably be made to work

[Yaël Dillies]

Yes, that's what I think too, but I don't know how doc-gen works.

[Eric Wieser]

It runs some markdown library then does some post-processing

[Bryan Gin-ge Chen]

It would probably be good to open a doc-gen issue about file links, even if it only serves as some temporary documentation about how we're currently linking files. I guess an even better option would be to add something about file links to our style guide.