Factory fields now mask lemmas and operators by default

[CohenCyril]

• former axioms can be recovered by prefixing with the module name,
• former theorems cannot, which causes major breakage when the library evolves.

[gares]

I guess one can make a local alias before shadowing, no?

[CohenCyril]

I guess one can make a local alias before shadowing, no?

The module approach we thought of does not work: no modules allowed inside sections.
Shadowing manually one by one is, meh, maybe we could have a HB command to shadow.

However, the problem is more general: I still would like to get a kind of "Absolute addressing" of library lemmas without distinction of whether they are axiom or theorem of one theory or another.

[gares]

before starting the section one could define a module Super containing aliases for all the stuff the factory shadows, so that one can refer to shadowed stuff via Super.foo. Would that work?

[CohenCyril]

before starting the section one could define a module Super containing aliases for all the stuff the factory shadows, so that one can refer to shadowed stuff via Super.foo. Would that work?

That could work,... but how to select all this stuff? Should we force the user to declare the theory of his structures in a HB.theory-declared module?

Oh no, ok, I understood now!!! You just read the factory fields 😆
Yes! let's do that!

[CohenCyril]

Let's also keep what I did. It is nice that the axioms can be referred to as members of any of the structure modules that contains the associated mixin. It is useful anyway.