Zulip Chat Archive

Stream: new members

Topic: goal turns into something odd

Patrick Thomas (Jul 07 2022 at 04:55):

The goal seems to randomly change to something that uses syntax from towards the end of the file.

Screenshot-from-2022-07-06-21-51-37.png

File: https://github.com/pthomas505/lean3/blob/e9112715254d70a097bb652def015a2b73aa4379/src/metalogic/pred.lean

Yakov Pechersky (Jul 07 2022 at 05:16):

Is this the congr' bug? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Extension.20showing.20goal.20for.20a.20separate.20lemma

Patrick Thomas (Jul 07 2022 at 05:22):

Hmm, I'm not sure. It seems to go away if I move the associated code (https://github.com/pthomas505/lean3/blob/e9112715254d70a097bb652def015a2b73aa4379/src/metalogic/pred.lean#L1680-L1782) to the bottom of the file.

Patrick Thomas (Jul 07 2022 at 05:23):

Or delete the code below the lemma being worked on.

Patrick Thomas (Jul 07 2022 at 05:30):

Yeah, it might be, or at least related. That is, removing the congr' in the code further up seems to fix it.

Patrick Thomas (Jul 07 2022 at 05:39):

I'm not sure I understand what I should do to avoid it though. Is there something I should use instead of congr'?

Yakov Pechersky (Jul 07 2022 at 05:42):

It's just a visual bug, the state of the proof is fine.

Patrick Thomas (Jul 07 2022 at 05:43):

Ok. Thank you.

Last updated: Dec 20 2023 at 11:08 UTC