porting attributes

Stream: lean4

[Scott Morrison]

Would anyone be able to show me how to implement a no-op attribute?

[Scott Morrison]

There are some attributes, particularly @[simps] used widely in mathlib3, that will need to be ported, but not quite yet.

[Scott Morrison]

In the meantime, I'd like to just have a no-op implementation, in the spirit of getting declarations to type-check even if proofs still fail.

[Scott Morrison]

I've had a look at @Gabriel Ebner's implemention of @[ext] in mathlib4. It seems he has to do something a bit hacky, because attributes aren't natively supported on structures. It leaves me unsure how to proceed. :-(

[Mac]

I am not sure exactly what you are asking, but to implement a simple no-op tag attribute all you need to do is just register the attribute. For example:

import Lean.Attributes

open Lean

initialize noopAttr : TagAttribute ←
  registerTagAttribute `noop "Example no-op attribute"

You can then use @[noop] as a tag in a file which imports this definition.

[Gabriel Ebner]

The best documentation is the lean4 source code: https://github.com/leanprover/lean4/blob/9ae6380b4332f49d5c4770a011e82de682cde624/src/Lean/Attributes.lean
(There's even comments!)

[Gabriel Ebner]

You can also look at the new nolint attribute for more inspiration.

[Gabriel Ebner]

Scott Morrison said:

I've had a look at Gabriel Ebner's implemention of @[ext] in mathlib4. It seems he has to do something a bit hacky, because attributes aren't natively supported on structures. It leaves me unsure how to proceed. :-(

This hack is only relevant for structures. There's literally check in core that says "throw an error unless the attribute is `class" for structures. I meant to report this, but things got in the way and it was easier to workaround.