error message from non-existent file

Stream: new members

[Michael Beeson]

inf8.lean:15:4
failed to instantiate goal with x
state:
M : Type,
_inst_1 : Model M,
x z y : M,
h1 : x ∈ 𝔽,
h2 : z ∈ 𝔽,
h3 : y ∈ 𝔽
⊢ (∃ (x_1 y_1 z_1 : M),
        ‹  ‹ x,z › ,single (single y) ›  =  ‹  ‹ x_1,y_1 › ,single (single z_1) ›  ∧
         ∀ (w : M),
           (∀ (b : M),  ‹  ‹ b,zero › ,single (single b) ›  ∈ w) →
           (∀ (a b c : M),  ‹  ‹ a,b › ,c ›  ∈ w →  ‹  ‹ a,𝕊 b › ,𝕊 c ›  ∈ w) →
            ‹  ‹ x_1,y_1 › ,z_1 ›  ∈ w) ↔
    x + z = y

But file inf8.lean does not even exist and there is no code like this in the
project. There was a file inf8 but I deleted it and even did lean project build again.
All the proofs compile OK but there is still this strange message! How can I get rid of it?

[Floris van Doorn]

weird... Does leanproject delete-zombies help? That deletes .olean files. without matching .lean files.

[Michael Beeson]

Yes, there was a zombie and that fixed it. Thanks!