Schrödinger's #synth

Stream: lean4

[Eric Wieser]

In Lean 4.11.0 ("Mathlib stable" in the web editor), this code both reports the decidable instance, and reports that such an instance cannot be synthesized

import Mathlib.Data.List.Infix

#synth Decidable ([1, 2].IsInfix [0, 1, 2, 3])

[Eric Wieser]

In Lean 4.12.0, the instance docs#List.decidableInfix looks to have been deleted accidentally when bumping mathlib (fixed in #17420).