Topological spaces doubt

Stream: Lean for the curious mathematician 2020

[Eloi]

I'm curious about the dots in this function, what are they for?

def of_basic {X : Type} (m : metric_space_basic X) : metric_space X :=
{ compatible := begin intros, refl, /- this should when the above parts are complete -/ end,
  ..m,
  ..@metric_space_basic.topological_space X m }

(The file is lftcm2020/src/exercises_sources/wednesday/afternoon/topological_spaces.lean)

[Kyle Miller]

For structure/record construction notation, ..m means to include all of m's fields.

[Eloi]

Thanks, why commenting them does not give a type error?

[Kyle Miller]

This is where the documentation for that notation should be, but it seems to be absent: https://leanprover.github.io/reference/declarations.html#id10 (I haven't been able to find where it's described...)

I'll check what you're saying about commenting it out.

[Kyle Miller]

Ah, in this case those are redundant because metric_space is defined to be a class (which is a structure with the [class] attribute and some special support for doing class things), so Lean is inferring the rest of the fields because metric_space extends topological_space and metric_space_basic, and these are already implemented by metric_space_basic through instances defined previously. Someone more knowledgeable than me would have a more informative answer -- I don't really know how this works expect through practice.

[Kyle Miller]

Try commenting out the compatible line to see the error you would normally get due to missing fields.

[Alex J. Best]

Nice catch, it looks like lean is smarter than I gave it credit for?!. Like Kyle says it knows how to fill these fields automatically given the available info. If you put #print of_basic after and compare the results of deleting and undeleting the lines you can see that although it changes the definition visually, what lean puts is equivalent but a more compact way of writing what my definition gave.

[Eloi]

Thanks!