Topic: How to add user attributes?
François G. Dorais (Jan 24 2021 at 00:17):
I've been enjoying Lean 4 a great deal and I'm really impressed by the powerful macro system which has so far helped me delay learning more about the deeper parts of Lean 4 metaprogramming. However, there are some things that are beyond the macro system. I know the docs aren't ready yet and I'm generally happy to wait... but Lean 4 is so exciting!
Perhaps this is not a wise place to get started learning about using the Lean 4 monads, but I thought I'd ask since I couldn't find any examples in the tests or elsewhere and there's a similar thing I want to do to port some old Lean 3 code. Let's say I want to add a simple tag attribute called
tellMeYourName such that
@[tellMeYourName] def blah := 0
prints out "My name is blah" (or some other inconsequential but observable action). How would I go about doing that in Lean 4?
Leonardo de Moura (Jan 25 2021 at 04:12):
Users will be able to define their own attributes. However, the attribute API is still changing. We will document and add examples as soon as it is stable.
Last updated: May 07 2021 at 11:09 UTC