Zulip Chat Archive

Stream: general

Topic: convert


view this post on Zulip Kenny Lau (May 31 2018 at 01:30):

maybe convert can automatically apply_instance?

view this post on Zulip Simon Hudon (May 31 2018 at 02:17):

Are you thinking in writing or asking for help?

view this post on Zulip Kenny Lau (May 31 2018 at 02:17):

I'm suggesting

view this post on Zulip Simon Hudon (May 31 2018 at 02:18):

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

view this post on Zulip Kenny Lau (May 31 2018 at 02:18):

sorry

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 31 2018 at 02:26):

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

view this post on Zulip Kenny Lau (May 31 2018 at 02:26):

e.g. finsupp.sum_zero_index


Last updated: May 16 2021 at 21:11 UTC