How are attributes defined?

Stream: lean4

[Yuri de Wit]

Where do attributes such as @[extern ...] or @[inline] comes from in Lean4? Are these basically built-in or part of a general strategy to allow custom metadata added to syntax elements? This question came up wondering whether they could be used to build a library for parsing command line arguments.

[Mario Carneiro]

They are syntactically elements of the attr syntax category, although many of them fall into a simple subcategory of the form ident : attr

[Arthur Paulino]

@Yuri de Wit maybe this can help you. extern is a parametric attribute (rather than a simple tag attribute that takes no parameters)

[Arthur Paulino]

More: https://github.com/leanprover/lean4/tree/master/src/Lean/Compiler

[Yuri de Wit]

Thanks, @Arthur Paulino and @Mario Carneiro ! I found the definitions for TagAttribute and ParametricAttribute and now have something to chase from here. I have never defined custom syntax/macros in Lean (in fact know practically nothing about Lean) and may come back with more questions.