initialize_simp_projections is sometimes a placebo

Stream: metaprogramming / tactics

[Robert Maxton]

Minor UX note, but:

import Mathlib.Tactic.Common

class HasInverse (f : α → β) : Prop where
  exists_inv_id : ∃ inv, f ∘ inv = ID ∧ inv ∘  f = id

initialize_simps_projections? HasInverse

gives

[simps.verbose] generating projection information for structure HasInverse.

[simps.verbose] generated projections for HasInverse:
    No lemmas are generated for the projections: exists_inv_id.

i.e. the tactic did nothing. It'd be cool if this gave a warning or something, since pretty much any time this happens it's probably certain that the user (cough like myself cough) is using it wrong. (In this case I thought it'd make lemmas for Prop-typed fields and didn't think to check until later.)