Stream: general

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

YH (Nov 25 2019 at 20:17):

Saw it in mathlib

Patrick Massot (Nov 25 2019 at 20:19):

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

Patrick Massot (Nov 25 2019 at 20:20):

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

YH (Nov 25 2019 at 20:46):

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

Thanks.

YH (Nov 25 2019 at 20:47):

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 (Nov 25 2019 at 20:52):

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 (Nov 25 2019 at 20:52):

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.

Last updated: May 10 2021 at 23:11 UTC