leanprover-community / leanprover-community/mathlib4

port and enhance `tfae` tactics

Open
#2,061 3 comments 0 reactions 1 assignee View on GitHub

@thorimur is already working on this.

Since Sep 20, 2024.

  • #2062 by @thorimur — closed without merging
t-meta
Dominant language
Lean
Stars
4.1k
Forks
1.7k
No merged PRs in 30d

Description

  • We need to port tfae_have and tfae_finish. We have basic versions for mathlib parity via #2062.

  • The internals could be made more efficient (e.g. by finding strongly connected components).

  • We'd also like to add a block tactic version of tfae, i.e. tfae with .... using | and =>.

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.