Missing simp in zero_toGame?

Stream: mathlib4

[Tristan Figueroa-Reid]

I am assuming this has a good reason, but I am wondering why zero_toGame does not have a simp attr when one_toGame does?

[Eric Wieser]

If you try adding it, I think #lint will complain

[Tristan Figueroa-Reid]

Eric Wieser said:

If you try adding it, I think #lint will complain

Doesn't seem to complain, unfortunately - unless I'm using it wrong.

#lint
@[simp]
theorem zero_toGame : toGame 0 = 0 :=
  rfl

gives me:

-- Found 0 errors in 64 declarations (plus 114 automatically generated ones) in the current file with 15 linters


-- All linting checks passed!

[Eric Wieser]

Those are separate commands, and you have them in the wrong order

[Eric Wieser]

#lint only checks the file so far, not things below it

[Eric Wieser]

Though I think in this case it would be appropriate to do it anyway and silence the linter, as this lemma is eligible for dsimp.

[Tristan Figueroa-Reid]

Adding it after reports finding 0 errors in 65 declarations (accounting for the zero_toGame decl), and adding it to the end of the file also reports 0 errors with 72 declarations.

[Eric Wieser]

Maybe the linter got smarter recently. A PR to add the attribute sounds good!

[Tristan Figueroa-Reid]

Eric Wieser said:

#lint only checks the file so far, not things below it

This does explain why I never caught CI lint errors locally! :sweat_smile:

[Violeta Hernández]

Yet again complaining about the lack of a ping!

[Violeta Hernández]

The reason this lemma isn't tagged simp is because it's redundant. If f : X ->+ Y then f 0 = 0 always, and there's some other simp lemma elsewhere that already states this.

[Eric Wieser]

I think my dsimp remark above still applies