Zulip Chat Archive

Stream: general

Topic: convert


Kenny Lau (May 31 2018 at 01:30):

maybe convert can automatically apply_instance?

Simon Hudon (May 31 2018 at 02:17):

Are you thinking in writing or asking for help?

Kenny Lau (May 31 2018 at 02:17):

I'm suggesting

Simon Hudon (May 31 2018 at 02:18):

There's no context accompanying your comment, it's in a brand new thread

Kenny Lau (May 31 2018 at 02:18):

sorry

Mario Carneiro (May 31 2018 at 02:25):

This doesn't make any sense. convert generates an equality goal, it is never something that can be apply_instance solvable

Kenny Lau (May 31 2018 at 02:26):

oh, convert generates auxiliary goals, some of which are apply_instance solvable

Kenny Lau (May 31 2018 at 02:26):

e.g. finsupp.sum_zero_index


Last updated: Aug 03 2023 at 10:10 UTC