!4#3063 – linter fails in 165 places

Stream: PR reviews

[Jeremy Tan]

image.png Is this another case of #2055, at !4#3063?

[Moritz Doll]

I would like to :ping_pong: this, I have no idea what is going on.

[Scott Morrison]

(The correct linkifier is lean4#2055.)

[Jeremy Tan]

Note that there are some dangerous instances in the ported file. We should merge !4#3139 and remove the dangerous instances first before going on

[Jeremy Tan]

!4#3063 can now be merged after the removal of dangerous instances, lean4#2055 was not there after all