Zulip Chat Archive

Stream: new members

Topic: error message from non-existent file

Michael Beeson (Oct 09 2020 at 02:11):

failed to instantiate goal with x
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 (Oct 09 2020 at 02:27):

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

Michael Beeson (Oct 09 2020 at 03:41):

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

Last updated: Dec 20 2023 at 11:08 UTC