Custom attributes

Stream: general

[Wojciech Nawrocki]

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]

Nvm found it,

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

[Wojciech Nawrocki]

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]

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]

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]

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.