abstract and opaque in the module declaration

[fredrik-bakke]

@lowasser @malarbol
Were you aware that it is possible to put the abstract and opaque words together with the where keyword in a module declaration? E.g.

module _
  {l : Level} {A : UU l}
  where opaque
  
  unfolding something
  
  is-prop-my-prop : is-prop my-prop
  is-prop-my-prop = ...

or

module _
  {l : Level} {A : UU l}
  where abstract
  
  is-prop-my-prop : is-prop my-prop
  is-prop-my-prop = ...

This is a pattern we don't currently use in the library, but which I believe we should use, especially now that we are taking these keywords more seriously. #1102 #1106 #1457 #1521 #1612

These keywords detract from the actual formalization and are not important to the reader, only the formalizer/implementer: an entry should mean the exact same to the reader whether it is abstract, opaque or transparent. As Martín Escardó more nicely put it recently in a mathstodon toot (which I am struggling to find atm), there's an inherent trade-off to using these keywords: on the one hand it helps the formalizer write and typecheck their code, and on the other hand it adds noise to the code that detracts the reader from the, shall we say, "essence". By using the pattern I propose above we reduce the noise, as the keywords take up less space, and we need less indentation.

I wanted to share this again even though it was discussed and rejected in the past. @VojtechStep