Zulip Chat Archive

Stream: lean4

Topic: How to add user attributes?

view this post on Zulip 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?

view this post on Zulip 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