Zulip Chat Archive

Stream: general

Topic: eq.rec docs


Reid Barton (Nov 15 2021 at 13:59):

Anyone know why there are no docs generated for docs#eq.rec?

Eric Wieser (Nov 15 2021 at 14:14):

We don't generate docs for any "autogenerated" lemmas

Reid Barton (Nov 15 2021 at 14:17):

oh weird

Reid Barton (Nov 15 2021 at 14:18):

I guess there are a lot of them, but X.rec seems important no? I mean there are many occurrences of eq.rec in the statements of other lemmas

Eric Wieser (Nov 15 2021 at 14:20):

I guess the argument is that .rec is "obvious" from the inductive declaration

Eric Wieser (Nov 15 2021 at 14:21):

Maybe we should have a collapsed panel of "subdeclarations" inside inductive boxes which shows all the autogenerated definitions like rec, rec_on, cases, ...

Floris van Doorn (Nov 15 2021 at 14:26):

It would be nice if eq.rec redirects to eq in the same way as docs#eq.refl does. I don't think we need to change the entry of eq to include information about eq.rec though.

Reid Barton (Nov 15 2021 at 14:29):

Having something to link to for eq.rec is useful for explaining to users of other proof assistants (why this just came up now for me).

Reid Barton (Nov 15 2021 at 14:30):

Maybe we can have some mechanism whereby we manually indicate to the documentation generator that it should include documentation for indicated autogenerated definitions (e.g. eq.rec, eq.rec_on but not the recursors for every random inductive type)

Eric Wieser (Nov 15 2021 at 14:30):

Or maybe just for rec that actually appear in statement of other lemmas?

Reid Barton (Nov 15 2021 at 14:31):

That also sounds reasonable but I am not sure if the documentation generator has access to that information at an appropriate time

Eric Wieser (Nov 15 2021 at 14:31):

If the lean exporter just wrote out all definitions including autogenerated ones (rather than filtering them out), then the python script could filter them back out again, at the point when it has all the information

Gabriel Ebner (Nov 15 2021 at 15:56):

We could try to include the auto-generated declarations in the documentation, but collapse them by default. (Not sure how much space they take up. There's also various kinds of auto-generated declarations, equation lemmas, no_confusion, injectivity lemmas, sizeof, sunfold, expansion of general inductive types, ...).

Yaël Dillies (Nov 15 2021 at 16:17):

Equation lemmas are already included as part of the definition, and also they have the same name as the corresponding definition so I wouldn't include them.

Eric Wieser (Nov 15 2021 at 16:19):

and also they have the same name as the corresponding definition

That's not true, they are called foo.equations._eqn_1. rw and simp just know how to desugar foo into that name

Alex J. Best (Nov 15 2021 at 16:21):

We already handle these in doc_gen by putting an "Equations" section after the def, so the proposal is just to do the same with "Auxiliary declarations" too right

Eric Wieser (Nov 15 2021 at 16:22):

Yes, although the "auxiliary declarations" will likely need explicit arguments unlike the equations which mostly just reuse the arguments of the parent

Eric Wieser (Nov 15 2021 at 16:38):

I guess we'd add all of these?
https://github.com/leanprover-community/mathlib/blob/ca61dbffa497f43e2bdf6c4c6f446c112043ecd1/src/meta/expr.lean#L1086-L1088

Gabriel Ebner (Nov 15 2021 at 16:53):

I think it could be helpful to show them. I don't how many people know all the auto-generated definitions, nevermind how they are defined.

Kyle Miller (Nov 15 2021 at 16:59):

I like this idea to make the autogenerated definitions more documented. I remember it being frustrating while learning when I'd follow definitions and hit one of them. It was very unclear what they were or what they were for, and there's not much that helps direct you to the answer (save asking Zulip or thinking to check the right textbook).

Would it be a good idea to modify #print so that it directs you to how an automatically generated definition was created? I imagine #print eq.rec could at the least be like

protected eliminator eq.rec : Π {α : Sort u} {a : α} {motive : α  Sort l}, motive a  Π { : α}, a =   motive 

Generated for the inductive type eq.

and maybe even point you to where in the Lean source code it's generated.

Kyle Miller (Nov 15 2021 at 17:02):

(Relatedly, sometimes I feel like it would be nice to have provenance information for other automatically generated objects, like things created by to_additive. Could there be something like a "from" attribute that the docs could include and linkify?)

Gabriel Ebner (Nov 15 2021 at 17:05):

We already have "to" attributes, so it could be enough to just reverse that map.

Junyan Xu (Nov 15 2021 at 20:42):

There are also lemmas semi-auto-generated by @[simps], reassoc, elementwise etc. which can be lengthy. For example, I'd rather have this collapsed.

Gabriel Ebner (Nov 15 2021 at 20:46):

I think that also needs open category_theory topological_space opposite, which is another reasonable feature request.


Last updated: Dec 20 2023 at 11:08 UTC