Finset in mathlib4_docs

Stream: mathlib4

[Flo (Florent Schaffhauser)]

In the documentation page Mathlib.Data.Finset.Basic, the entry structure Finset says :

structure Finset
(α : Type u_4) :
Type u_4
val : Multiset α
The underlying multiset
nodup : Nodup s. val
val contains no duplicates

while the source says:

structure Finset
(α  :  Type *)  where
  /-- The underlying multiset -/
  val  :  Multiset α
  /-- `val` contains no duplicates -/
  nodup :  Nodup val

Isn't s.val incorrect in the doc page? Shouldn't it say Multiset.Nodup val instead?

Of course, there are other discrepancies between the doc and the code, for instance Type u_4 instead of Type*, so maybe I am misunderstanding how the doc page is generated from the source. If so, I'd be happy to hear if there is a reason why s.val is okay there :blush:

[Yaël Dillies]

Hmm you're right, that's weird... Do you have other examples like that?

[Flo (Florent Schaffhauser)]

I'm afraid I don't, I bumped into that randomly.

[Yaël Dillies]

cc @Henrik Böving

[Henrik Böving]

The Type u_4 is normal and not something I can do anything about. u_4 is a universe variable that was automatically introduced since you were too lazy to name it with Type*. If you want this to render differently, that's a core issue.

The s.val issue is probably (I won't be on a lean machine until the evening to verify this) the s from this line: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Process/StructureInfo.lean#L23 which is used to figure out the type of the field...I dont really know how I could refactor this code to make the s disappear fully? I could name it "self" instead, in the spirit of python etc.

Other than that if you want this to disappear a better meta programmer than me will have to do the job.

[Henrik Böving]

Oh and "the reason" s.val shows up here, if you can't read meta: To print out the type of a structure field we assume there exists some value s of that structure type and then print the type of s.field.

[Flo (Florent Schaffhauser)]

Henrik Böving said:

The Type u_4 is normal and not something I can do anything about. u_4 is a universe variable that was automatically introduced since you were too lazy to name it with Type*.

I don't get it :sweat_smile: Did I do something something wrong? Why was I lazy? :flushed:

The s.val issue is probably (I won't be on a lean machine until the evening to verify this) the s from this line: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Process/StructureInfo.lean#L23 which is used to figure out the type of the field...I dont really know how I could refactor this code to make the s disappear fully? I could name it "self" instead, in the spirit of python etc.

Yes, I thought about interpreting s.val as self.val, but then I was still surprised by the discrepancy between the docs and the source, so I became curious.

Other than that if you want this to disappear a better meta programmer than me will have to do the job.

I don't want it to disappear, I was just wondering if I may be misunderstanding something. And I certainly did not imply anything else :smile: Thank you very much for your explanations!

[Ruben Van de Velde]

"lazy" is perhaps a bit of a strong word. Type* is the (encouraged) syntax for "make up a universe variable u_xxx and replace me by Type u_xxx", so that's what you see in the output