issue !4#10759: Porting note: removed `@[simp]` to avoid ...

Stream: triage

[Random Issue Bot]

Today I chose issue 10759 for discussion!

Porting note: removed @[simp] to avoid a simpNF linter error
Created by @Pietro Monticone (@pitmonticone) on 2024-02-20
Labels: porting-notes

Is this issue still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

It seems that all the porting notes referencing this issue (search for -- Porting note (#10619). Yes they are referencing the wrong issue) are outdated, but I'll let @David Ang decide

[David Ang]

The porting notes mentioned in the issue can all be safely deleted

[Yaël Dillies]

#17648