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(category_theory/monoidal): coherence tactic #13125

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat(category_theory/monoidal): coherence tactic #13125

wants to merge 19 commits into from

Commits on Apr 2, 2022

  1. starting

    @semorrison
    semorrison committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    c42c3a9 View commit details
    Browse the repository at this point in the history

  2. feat(category_theory/monoidal): coherence tactic

    @semorrison
    semorrison committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    48b399b View commit details
    Browse the repository at this point in the history

  3. minor

    @semorrison
    semorrison committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    308b5f4 View commit details
    Browse the repository at this point in the history

  4. cleanup

    @semorrison
    semorrison committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    3217c62 View commit details
    Browse the repository at this point in the history

  5. minor

    @semorrison
    semorrison committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    61b7a3c View commit details
    Browse the repository at this point in the history

  6. reformulate a proof using the coherence tactic

    @semorrison
    semorrison committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    88475d0 View commit details
    Browse the repository at this point in the history

  7. another

    @semorrison
    semorrison committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    4756883 View commit details
    Browse the repository at this point in the history

  8. Update src/category_theory/monoidal/coherence.lean 

    Co-authored-by: Oleksandr Manzyuk <manzyuk@gmail.com>
    @semorrison @manzyuk
    semorrison and manzyuk committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    86cf104 View commit details
    Browse the repository at this point in the history

  9. lint

    @semorrison
    semorrison committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    f336001 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'semorrison/coherence' of github.com:leanprover-communit… 

    …y/mathlib into semorrison/coherence
    @semorrison
    semorrison committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    7b34723 View commit details
    Browse the repository at this point in the history

Commits on Apr 3, 2022

  1. suggestion from review

    @semorrison
    semorrison committed Apr 3, 2022
    Configuration menu
    Copy the full SHA
    71219bd View commit details
    Browse the repository at this point in the history

  2. refactoring suggestions from Yuma

    @semorrison
    semorrison committed Apr 3, 2022
    Configuration menu
    Copy the full SHA
    858bc3c View commit details
    Browse the repository at this point in the history

  3. add comment about search depth

    @semorrison
    semorrison committed Apr 3, 2022
    Configuration menu
    Copy the full SHA
    48ccdb1 View commit details
    Browse the repository at this point in the history

  4. add test

    @yuma-mizuno
    yuma-mizuno committed Apr 3, 2022
    Configuration menu
    Copy the full SHA
    f6a8703 View commit details
    Browse the repository at this point in the history

  5. Revert "refactoring suggestions from Yuma" 

    This reverts commit 858bc3c.
    @semorrison
    semorrison committed Apr 3, 2022
    Configuration menu
    Copy the full SHA
    81d282e View commit details
    Browse the repository at this point in the history

  6. update test

    @semorrison
    semorrison committed Apr 3, 2022
    Configuration menu
    Copy the full SHA
    07b59af View commit details
    Browse the repository at this point in the history

Commits on Apr 5, 2022

  1. throw in a dsimp at monoidal_coherence

    @semorrison
    semorrison committed Apr 5, 2022
    Configuration menu
    Copy the full SHA
    8f0dacb View commit details
    Browse the repository at this point in the history

  2. internally increase the typeclass search depth

    @semorrison
    semorrison committed Apr 5, 2022
    Configuration menu
    Copy the full SHA
    45a1092 View commit details
    Browse the repository at this point in the history

Commits on Apr 9, 2022

  1. Apply suggestions from code review 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @semorrison @jcommelin
    semorrison and jcommelin committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    afffac0 View commit details
    Browse the repository at this point in the history