Zulip Chat Archive

Stream: general

Topic: convert_to vs convert

Mario Carneiro (Aug 13 2021 at 23:56):

Looking at the documentation for convert_to , it's not clear how it differs from convert. The documentation also spends most of its text talking about ac_change instead for some reason, and the code example uses ac_change.

Mario Carneiro (Aug 14 2021 at 00:07):

Aha, from the original PR: https://github.com/leanprover-community/mathlib/pull/944#issuecomment-483903992

Last updated: Dec 20 2023 at 11:08 UTC