tactic.converter.binders

Stream: general

[Yury G. Kudryashov]

What is the purpose of this file?

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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.

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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

[Mario Carneiro]

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