missing attributes

Stream: mathlib4

[Patrick Massot]

During the port, what should we do when Lean complains an attribute doesn't exist?

[Patrick Massot]

Specifically, what about refl and trans?

[Scott Morrison]

For refl:

import Mathlib.Tactic.Relation.Rfl

@[refl]
theorem foo : 1 = 1 := rfl

[Scott Morrison]

For trans, for now use import Mathlib.Mathport.Attributes, I guess.

[Scott Morrison]

If you run into other attributes, hopefully you will find them noted as needing porting in Mathlib/Mathport/Syntax.lean (which you can freely import if needed, I guess), or they should already be implemented somewhere, and searching for register.*attr should help you locate it.

[Patrick Massot]

@Mario Carneiro do you agree with all this?