Generating equations in `DeclCache`

Stream: batteries

[Snir Broshi]

If I understand correctly, DeclCache.mk builds a cache of all the available getEnv.constants.

constants is a map from names to Lean.ConstantInfo, and some constants are definitions (ConstantInfo.defnInfo variant).

These constants are definitions that have corresponding lazily autogenerated equations, that can be generated by calling getEqnsFor? on the constant's name, like docgen does.

I propose forcing all equations to generate and adding them to the cache by calling getEqnsFor? in DeclCache.mk. The motivation is seeing all equations on Loogle. Are there other users of DeclCache which this change might break? Maybe adding (addEqnDecl : Name → ConstantInfo → α → MetaM α) parameter to DeclCache.mk is a good solution, and default that parameter to a no-op.

Thoughts?