Zulip Chat Archive

Stream: general

Topic: Custom attributes

Wojciech Nawrocki (Feb 06 2019 at 21:51):

How would I go about defining custom attributes? The reference mentions: The set of attributes is open-ended since users can declare additional attributes in Lean (see Chapter 7., but Chapter 7 is empty :cry:

Wojciech Nawrocki (Feb 06 2019 at 21:54):

Nvm found it,

meta def foo_attr : user_attribute := { name := `foo, descr := "bar" }`

Wojciech Nawrocki (Feb 06 2019 at 22:33):

Hm no, that doesn't seem to work with simp. What I would like to do is define custom attributes, say e.g. a cnf, so that I can tag lemmas which bring Boolean expressions into CNF form with @[cnf] and then use simp with cnf to convert into CNF. But simp throws an error of the form unknown identifier simp_attr.cnf when I try that. The only reference to that seems to be here but I don't understand the kernel well enough to figure out how to define simp attrs from that.

Wojciech Nawrocki (Feb 06 2019 at 22:54):

Really found it this time I think, run_cmd mk_simp_attr ``cnf [``simp]. Probably not supposed to do this, but it seems to work.

Kevin Buzzard (Feb 06 2019 at 23:25):

https://github.com/leanprover-community/mathlib/blob/c9e4f8edc30da76ffa740000957e26aaf79cc31e/docs/tactics.md#apply_rules is the only place I've seen this sort of thing covered. For some aspects of Lean coding, those user docs are essential. I found that link by searching for user_attribute in the repo.

Wojciech Nawrocki (Feb 08 2019 at 18:59):

I didn't see that, thanks! Later I found this file which suggests that user simp attributes are perfectly fine, and I like the mechanism because it can apply to hypotheses as well.

Last updated: Aug 03 2023 at 10:10 UTC