Zulip Chat Archive

Stream: general

Topic: declaration uses sorry bug


view this post on Zulip Johan Commelin (Jan 14 2021 at 19:26):

I have the error declaration 'foobar' uses sorry but...
I don't get any red squiggles, and I have a "Goals accomplished :tada:" at the end of my proof.
How do I debug this?

view this post on Zulip Eric Wieser (Jan 14 2021 at 19:44):

Does that happen if you depend on another declaration that uses sorry?

view this post on Zulip Bryan Gin-ge Chen (Jan 14 2021 at 19:45):

Does docs#tactic.interactive.recover do anything?

view this post on Zulip Johan Commelin (Jan 14 2021 at 20:05):

aha... the lemma used a definition X, and X was defined as Y quux bar sorry, where the sorry filled in some proof obligation

view this post on Zulip Johan Commelin (Jan 14 2021 at 20:05):

after fixing that sorry, the error/warning was gone.


Last updated: May 14 2021 at 22:15 UTC