bikeshedding about #synth

Stream: general

[Kevin Buzzard]

Which is a better comment in a module docstring:

example {V : Type*} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V] :
    LieGroup 𝓘(𝕜, V →L[𝕜] V) (V →L[𝕜] V)ˣ := by infer_instance

or

variable {V : Type*} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V] in
#synth LieGroup 𝓘(𝕜, V →L[𝕜] V) (V →L[𝕜] V)ˣ

? I changed from example to #synth whilst also tinkering with typeclasses in #13709 but it was pointed out that maybe #synth is more complicated to understand.

[Damiano Testa]

I think that I would prefer

variable {V : Type*} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V] in
#synth LieGroup 𝓘(𝕜, V →L[𝕜] V) (V →L[𝕜] V)ˣ  --Units.instLieGroupModelWithCornersSelf

[Damiano Testa]

This is certainly what I prefer to see when I am debugging something, in order to find out what the instance actually is and then I can go and look at it.

[Michael Rothgang]

I asked this question on #13709 - if there's a clear preference in this thread, I'm very happy to go with that.

[Kevin Buzzard]

When I get to a computer I can add the instance name as a comment

[Kyle Miller]

I don't really like the idea of including the instance name docs#Units.instLieGroupModelWithCornersSelf since it's autogenerated and not meant to be used in source files.

I think if you want to refer to it, you should give the instance an explicit name. I would leave it as an example since it's easier to understand and you can be sure you know what it's meaning to show. (For example, I had to check the source code of #synth just now to verify some of its behavior.)

[Kyle Miller]

Here's an alternative: use instance in the docstring.

instance {V : Type*} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V] [Nontrivial V] :
    LieGroup 𝓘(𝕜, V →L[𝕜] V) (V →L[𝕜] V)ˣ := inferInstance

This shows that this is a superfluous instance since it's already covered.