search

leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

Put inductive/structure documentation before field documentation #161

Closed nomeata closed 9 months ago

nomeata commented 9 months ago

Consider a user trying to find out what Std.Format is. They navigate to

https://leanprover-community.github.io/mathlib4_docs/Init/Data/Format/Basic.html#Std.Format

and the first thing they read is that .nil is “The empty format”. Only a good page further down, and separated from the last constructor’s doc with only an easy-to-miss change of indentation and font size, they find

A string with pretty-printing information for rendering in a column-width-aware way.

The pretty-printing algorithm is based on Wadler's paper A Prettier Printer.

Would it be possible to put the main documentation for the structure/inductive before the fields? See maybe the Haskell docs for inspiration.

hargoniX commented 9 months ago

Originally we used to have the ctor documentation above the ctor type but that was changed by @eric-wieser. If we do this change of swapping the whole type docs above the thing, would it be sensible to also reswap the ctor doc? And what do you, Eric, think about switching the type doc above given that you originally advocated for the ctor doc switch?

eric-wieser commented 9 months ago

I still firmly believe that constructors and fields names should be shown before their descriptions. I don't think I ever expressed an opinion on where the main docstring belongs, beside it appearing somewhere after the name.

nomeata commented 9 months ago

So inductive name, type, docs, followed by list of ctor, type, docs makes sense, does it?