Zulip Chat Archive

Stream: general

Topic: instance name tip

Kevin Buzzard (May 01 2021 at 22:54):

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:

Last updated: Aug 03 2023 at 10:10 UTC