## Stream: general

### Topic: tactic.converter.binders

#### Yury G. Kudryashov (May 01 2020 at 01:18):

What is the purpose of this file?

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

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

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

#### Yury G. Kudryashov (May 01 2020 at 01:44):

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

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

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

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