symm

Stream: mathlib4

[Jakob von Raumer]

Are we missing a

attribute [symm] Eq.symm

somewhere?

[Mario Carneiro]

this is an issue in the current implementation. There isn't any place you can place that attribute: it needs to be in the same file as the declaration, but it can't be in core unless the symm attribute itself is defined in core

[Kevin Buzzard]

Why does it need to be in the same file as the declaration?

[Jakob von Raumer]

It works fine if I put it in the file where I need it, so I'm pretty sure It would work if we put it in one of the topmost mathlib4 files

[Mario Carneiro]

There are several different kinds of attributes in lean 4. The simplest kind is called a "tag attribute", which is basically a marker on certain definitions: are you tagged or not. It is good for a lot of things like @[inline], @[reducible], @[instance]. One nice thing about tag attributes is that they have zero start-up cost - you just look in the file with the definition and see if it's tagged - but that means that they can only be tagged from the same file, since if you can tag a declaration from anywhere then either you have to look everywhere for tags or you have to spend some start up time on aggregating all the tags that have been placed on anything.

[Mario Carneiro]

Based on Jakob's observation, I think @[symm] is not a tag attribute but instead builds up a data structure at initialization time. @[simp] is the most complex of these kinds of attributes, and a large percentage of the few seconds it takes to import Mathlib are due to building the initial simp set

[Scott Morrison]

I've added this attribute already in https://github.com/leanprover-community/mathlib4/pull/856.