## 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?

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

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: May 16 2021 at 21:11 UTC