Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: tfae tactics #2062

Closed
wants to merge 23 commits into from
Closed

[Merged by Bors] - feat: tfae tactics #2062

wants to merge 23 commits into from

Commits on Feb 4, 2023

  1. start: create TFAE.lean

    @thorimur
    thorimur committed Feb 4, 2023
    Configuration menu
    Copy the full SHA
    e846238 View commit details
    Browse the repository at this point in the history

Commits on Feb 5, 2023

  1. feat: tfae_have and tfae_finish

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    0ae6f2f View commit details
    Browse the repository at this point in the history

  2. test: basic tfae tests

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    c9eb315 View commit details
    Browse the repository at this point in the history

  3. chore: minor cleanup

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    8449ffa View commit details
    Browse the repository at this point in the history

  4. chore: update Mathlib.lean

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    476df42 View commit details
    Browse the repository at this point in the history

  5. docs: module docstring

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    ea75fbc View commit details
    Browse the repository at this point in the history

  6. docs: tfae_have

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    6cd9bcf View commit details
    Browse the repository at this point in the history

  7. chore: minor docs and error messages

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    438ea0c View commit details
    Browse the repository at this point in the history

  8. docs: tfae_finish

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    e145384 View commit details
    Browse the repository at this point in the history

  9. docs: minor cleanup

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    be384c0 View commit details
    Browse the repository at this point in the history

  10. chore: copyright header

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    8ba2bcd View commit details
    Browse the repository at this point in the history

  11. chore: fix namespace

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    36ae3c1 View commit details
    Browse the repository at this point in the history

  12. docs: docstrings

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    ebd9dcd View commit details
    Browse the repository at this point in the history

  13. chore: clarify names

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    48b6b52 View commit details
    Browse the repository at this point in the history

  14. chore: fix Mathlib.lean order

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    b7b6a31 View commit details
    Browse the repository at this point in the history

  15. test: expand tests (trivial cases, context)

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    5324a66 View commit details
    Browse the repository at this point in the history

  16. chore: fix package name

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    31c86a6 View commit details
    Browse the repository at this point in the history

  17. chore: cleanup goal management

    @thorimur
    thorimur committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    4742080 View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2023

  1. chore: sections and misc. cleanup

    @thorimur
    thorimur committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    882bd0d View commit details
    Browse the repository at this point in the history

Commits on Feb 15, 2023

  1. Merge remote-tracking branch 'origin/master' into tfae

    @thorimur
    thorimur committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    e6ec9a3 View commit details
    Browse the repository at this point in the history

Commits on Feb 17, 2023

  1. docs: fix usage demonstration syntax

    @thorimur
    thorimur committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    3aa9b08 View commit details
    Browse the repository at this point in the history

  2. chore: delete tfae from Syntax.lean

    @thorimur
    thorimur committed Feb 17, 2023
    Configuration menu
    Copy the full SHA
    503b880 View commit details
    Browse the repository at this point in the history

Commits on Feb 20, 2023

  1. Merge remote-tracking branch 'origin/master' into tfae

    @thorimur
    thorimur committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    c497c65 View commit details
    Browse the repository at this point in the history