Zulip Chat Archive

Stream: general

Topic: Convert trace


view this post on Zulip Chris Hughes (Apr 22 2019 at 16:51):

Is there a trace for convert, or a version that doesn't use subsingleton elimination? I'm trying to debug.

view this post on Zulip Mario Carneiro (Apr 22 2019 at 16:53):

convert is just a wrapper around congr, so try to write in terms of congr first

view this post on Zulip Mario Carneiro (Apr 22 2019 at 16:53):

debugging congr is a bit tricky, but you can call the congr_lemma generator manually to see what you get

view this post on Zulip Chris Hughes (Apr 22 2019 at 17:11):

What do I do to trace a congr_lemma in a useful way?


Last updated: May 11 2021 at 13:22 UTC