Zulip Chat Archive

Stream: general

Topic: tactic.converter.binders


view this post on Zulip Yury G. Kudryashov (May 01 2020 at 01:18):

What is the purpose of this file?

view this post on Zulip Bryan Gin-ge Chen (May 01 2020 at 01:25):

Seems like part of an alternate version of conv mode? For comparison: https://github.com/leanprover-community/lean/tree/master/library/init/meta/converter

view this post on Zulip Bryan Gin-ge Chen (May 01 2020 at 01:34):

This is the oldest version I could find in the commits. Apparently it came from library_dev, which I guess is one of the precursors to mathlib.

view this post on Zulip Mario Carneiro (May 01 2020 at 01:38):

If you want to keep tracking the history, library_dev is at https://github.com/avigad/library_dev

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 01:44):

OK, let me reformulate. Zero files import it. Should we remove it?

view this post on Zulip Bryan Gin-ge Chen (May 01 2020 at 01:46):

What's the difference between old_conv and the current conv mode. Is there anything in the old_conv namespace that is worth keeping?

view this post on Zulip Mario Carneiro (May 01 2020 at 02:12):

the reason I kept it is exactly because I didn't have the time to understand the code, make sure it runs properly, and see what was available so we could make sure we have adequate replacements for everything

view this post on Zulip Mario Carneiro (May 01 2020 at 02:12):

I think Johannes wrote it but I've never heard the story of how it was written


Last updated: May 14 2021 at 22:15 UTC