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: Dec 20 2023 at 11:08 UTC