instance name tip

Stream: general

[Kevin Buzzard]

Well blow me down if I didn't just discover completely by accident a trick to solve a problem which has annoyed me for years.

Sometimes I am staring at code which says

instance (R : Type*) [comm_ring R] (Gᵢ : ℤ → add_subgroup R)
  [has_add_subgroup_decomposition Gᵢ] [add_subgroup.is_gmonoid Gᵢ] :
  algebra (zero_piece_subring Gᵢ) (nonneg_piece_subring_of_int_grading Gᵢ) := ...

or whatever, and thinking "I wish I knew the explicit name of that instance" (e.g. so I can explicitly feed it somewhere else). The algorithm to generate instance names is something I've never been on top of (and at least in the past depended on whether we were in the root namespace or not, although this might have changed recently).

Here's a stupid hack: just replace the def after the := by sorry #exit and then instance gets underlined in orange, and when you click on it, it says declaration 'direct_sum.has_add_subgroup_decomposition.nonneg_piece_subring_of_int_grading.algebra' uses sorry :tada: