Convert trace

Stream: general

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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