Zulip Chat Archive

Stream: general

Topic: convert, refl


Reid Barton (Nov 27 2018 at 15:47):

This is a new one for me--convert left a goal which I could close with refl

Patrick Massot (Nov 27 2018 at 15:52):

You can easily play with convert and, especially congr' code, they are easy to understand, as long as you don't try to understand what congr_core is doing, which I suspect you won't need to try

Reid Barton (Nov 27 2018 at 15:53):

Maybe refl closed some later goal, fixing a metavariable, and that caused an earlier goal to also be closable by refl

Reid Barton (Nov 27 2018 at 15:54):

I do have a _ in the argument to convert


Last updated: Dec 20 2023 at 11:08 UTC