inductive types in documentation

Stream: general

[Kyle Miller]

(moved from https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/class.20inductive/near/357876687)

Nice, that's better.

For inductive types, I wonder if it would be easier to read if it looked like this, with the docstrings below the constructors?

image.png

That would match how for normal top-level declarations the docstring is shown after the type.

[Henrik Böving]

Hm, I designed it so that it looks like the code that was written since that is basically the entire theme of doc-gen. So I think this would in fact be more confusing than helpful since it is not the syntax that the actual thing uses.

[Eric Wieser]

Well normal docstrings are written before the declaration, but appear in the docs as after

[Kyle Miller]

The way these are laid out I find to be difficult to read:

image.png

image.png

Having the | being where it isn't correct.

[Kyle Miller]

I think there's a case to be made that comments aren't syntax (they're a lexical feature, but they're not parsed), and docgen isn't representing all the lexical features of the comments anyway (where are the /-- and -/?), so it's fair to rearrange them.

[Kyle Miller]

Consider also consistency with how IDEs tend to display docstrings:

image.png

[Kyle Miller]

I think having docstrings come before declarations in the source is a concession anyway. They're less useful after since the source contains the body of the definition so you might have to scroll down to see it, and I'm not sure there's a reasonable way for them to be inside declarations Python-style. Ideally you'd know what's being documented if you come across a long docstring.

[Eric Wieser]

It's perhaps also worth noting that | isFalse {p : Prop} →¬p →Decidable p already fails at representing the source, as p is an index for the family not a constructor argument (I might have the wrong names here)

[Kyle Miller]

It's a parameter for the family. I wonder if it'd be reasonable to have docgen skip the parameters for constructors and re-use the parameter names from the inductive type itself?

[Eric Wieser]

Having the full type, especially WRT argument explicitness (as we do now) is arguably more useful as a caller; but maybe there's a compromise here somewhere

[Kyle Miller]

Maybe constructors could display using declaration signature style, and maybe it could also gray out parameters by virtue of them being implicit arguments.

So like this, with {p : Prop} gray

| isFalse {p : Prop} (h : ¬p) : Decidable p

[Eric Wieser]

In mathlib3 the docs already gray out implicit parameters

[Eric Wieser]

So you'd need a different discriminator here

[Eric Wieser]

(also, someone who is not on mobile should split this thread)

[Notification Bot]

14 messages were moved here from #general > class inductive by Kyle Miller.

[Kyle Miller]

Yeah, that's what I mean, just rely on the fact that implicit arguments are grayed out. I'm not sure if you really need to know which arguments are the inductive parameters

[Eric Wieser]

You need to know it when writing induction tactic cases

[Henrik Böving]

Eric Wieser said:

It's perhaps also worth noting that | isFalse {p : Prop} →¬p →Decidable p already fails at representing the source, as p is an index for the family not a constructor argument (I might have the wrong names here)

This is regardless the correct type of the constructor, it needs to get this as an implicit argument. I dont know whether it is possible to write an analysis that just skips this?

[Kyle Miller]

There are a number of places you can get the number of parameters, docs4#Lean.ConstructorVal.numParams for one.

[Kyle Miller]

You can use Lean.Meta.forallBoundedTelescope on the constructor's type using the number of parameters before you pretty print

[Kyle Miller]

I suppose one way to represent this is

| isFalse {p : Prop} : ¬p → Decidable p

with the parameters before the :. That way you see the correct type for the constructor, and you also get a bit more information about which are the parameters.

[Mac Malone]

Kyle Miller said:

I think there's a case to be made that comments aren't syntax (they're a lexical feature, but they're not parsed)

Dropped in here from Kyle's recent reference to this thread. I thought it might be worth noting that in Lean, docstring comments are parsed with a standard parser that produces a Syntax node just like any other node in the grammar. Thus, they can be analyzed and reproduced like normal syntax and unlike normal comments. On the other hand, the comment body does use a raw parser, so it is still a bit special.