Zulip Chat Archive

Stream: mathlib4

Topic: tfae Tfae TFEA

Johan Commelin (Jan 05 2023 at 18:26):

What's going to be the mathlib4 spelling? mathlib4#1354 uses Tfae, but I could also imagine TFAE...

Sky Wilshaw (Jan 05 2023 at 18:27):

I think TFAE is probably better. I'm the author of the PR, I'll change it unless anyone objects.

Sky Wilshaw (Jan 05 2023 at 18:27):

I also need to change the spelling of tfae in the docstring.

Johan Commelin (Jan 05 2023 at 18:27):

Is the tactic already ported?

Johan Commelin (Jan 05 2023 at 18:27):

Or does the tactic depend on this file?

Sky Wilshaw (Jan 05 2023 at 18:28):

I don't think the tactic is already ported. mathlib3 docs says it depends on this file. image.png

Sky Wilshaw (Jan 05 2023 at 18:30):

Should the file name also change to TFAE.lean?

Sky Wilshaw (Jan 05 2023 at 18:33):

I think I'll change it - we already have things like Data/Int/GCD.lean.

Eric Wieser (Jan 05 2023 at 18:56):

Do we have any tooling to convert between mathlib3 and mathlib4 filenames?

Eric Wieser (Jan 05 2023 at 18:56):

The yaml file doesn't have this information I don't think

Yury G. Kudryashov (Jan 28 2023 at 17:07):

Is there any progress with porting the tactic?

Yury G. Kudryashov (Jan 28 2023 at 17:08):

I'm porting a file that uses this tactic.

David Renshaw (Jan 28 2023 at 17:41):

According to the tactic port tracking issue, nobody is currently working on it. https://github.com/leanprover-community/mathlib4/issues/430

Last updated: Dec 20 2023 at 11:08 UTC