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(set_theory/game): short games, boards, and domineering #1540

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat(set_theory/game): short games, boards, and domineering #1540

wants to merge 14 commits into from

Commits on Oct 12, 2019

  1. feat(set_theory/game): short games, boards, and domineering

    @semorrison
    semorrison committed Oct 12, 2019
    Configuration menu
    Copy the full SHA
    ed4c53e View commit details
    Browse the repository at this point in the history

Commits on Oct 13, 2019

  1. simplifying succ_ne_self

    @semorrison
    semorrison committed Oct 13, 2019
    Configuration menu
    Copy the full SHA
    6f28d04 View commit details
    Browse the repository at this point in the history

  2. cleanup

    @semorrison
    semorrison committed Oct 13, 2019
    Configuration menu
    Copy the full SHA
    b4812b3 View commit details
    Browse the repository at this point in the history

Commits on Feb 28, 2020

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

    @semorrison
    semorrison committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    308291f View commit details
    Browse the repository at this point in the history

  2. remove old comment

    @semorrison
    semorrison committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    d155201 View commit details
    Browse the repository at this point in the history

  3. functions renamed

    @semorrison
    semorrison committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    130ce6a View commit details
    Browse the repository at this point in the history

Commits on Mar 2, 2020

  1. advice from linters

    @semorrison
    semorrison committed Mar 2, 2020
    Configuration menu
    Copy the full SHA
    f79b144 View commit details
    Browse the repository at this point in the history

Commits on Mar 27, 2020

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

    @semorrison
    semorrison committed Mar 27, 2020
    Configuration menu
    Copy the full SHA
    cbd3994 View commit details
    Browse the repository at this point in the history

  2. update for Lean 3.7

    @semorrison
    semorrison committed Mar 27, 2020
    Configuration menu
    Copy the full SHA
    8575cae View commit details
    Browse the repository at this point in the history

Commits on Apr 12, 2020

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

    Scott Morrison committed Apr 12, 2020
    Configuration menu
    Copy the full SHA
    b1c4506 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @semorrison @bryangingechen
    semorrison and bryangingechen committed Apr 12, 2020
    Configuration menu
    Copy the full SHA
    79b5fa6 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'domineering' of github.com:leanprover-community/mathlib… 

    … into domineering
    Scott Morrison committed Apr 12, 2020
    Configuration menu
    Copy the full SHA
    663a552 View commit details
    Browse the repository at this point in the history

  4. line lengths

    Scott Morrison committed Apr 12, 2020
    Configuration menu
    Copy the full SHA
    ccdaef0 View commit details
    Browse the repository at this point in the history

  5. oops, one more long line

    Scott Morrison committed Apr 12, 2020
    Configuration menu
    Copy the full SHA
    aa92843 View commit details
    Browse the repository at this point in the history