What do @[ext] @[simp] do?

Stream: general

[YH]

Saw it in mathlib

[Patrick Massot]

The answer is in the same doc file that Reid pointed out when answering your previous question.

[Patrick Massot]

(We don't mind questions, I'm only pointing out how you can help yourself)

[YH]

The answer is in the same doc file that Reid pointed out when answering your previous question.

Thanks.

[YH]

The answer is in the same doc file that Reid pointed out when answering your previous question.

Where can I find some general tutorial on attributes? Searching "lean attribute" doesn't help much.

[Floris van Doorn]

Here is some information about attributes in general:
https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html?highlight=attribute#attributes

[Floris van Doorn]

If the attribute has been defined in mathlib, then the meaning of that attribute is very likely to be explained in the aforementioned tactics.md.