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] - chore: refactor of Algebra/Group/Defs to reduce imports #9606

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - chore: refactor of Algebra/Group/Defs to reduce imports #9606

wants to merge 16 commits into from

Commits on Jan 10, 2024

  1. chore: refactor of Algebra/Group/Defs to reduce imports

    @kim-em
    kim-em committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    e8b47c7 View commit details
    Browse the repository at this point in the history

  2. cleanup

    @kim-em
    kim-em committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    364c7ad View commit details
    Browse the repository at this point in the history

  3. add module doc

    @kim-em
    kim-em committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    3708d35 View commit details
    Browse the repository at this point in the history

  4. .

    @kim-em
    kim-em committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    a42bf4a View commit details
    Browse the repository at this point in the history

  5. import all

    @kim-em
    kim-em committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    57f470d View commit details
    Browse the repository at this point in the history

  6. fix test

    @kim-em
    kim-em committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    ee102fe View commit details
    Browse the repository at this point in the history

Commits on Jan 11, 2024

  1. Apply suggestions from code review 

    Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
    @kim-em @Vierkantor
    kim-em and Vierkantor authored Jan 11, 2024
    Configuration menu
    Copy the full SHA
    beb8163 View commit details
    Browse the repository at this point in the history

  2. import Tactic.TypeStar and Tactic.Lemma in Tactic.Basic

    @kim-em
    kim-em committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    fc94448 View commit details
    Browse the repository at this point in the history

  3. import assert_not_exists

    @kim-em
    kim-em committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    ecddcee View commit details
    Browse the repository at this point in the history

  4. cleanup

    @kim-em
    kim-em committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    3fd2844 View commit details
    Browse the repository at this point in the history

  5. move lemmas into Group/Basic per Yaël's request

    @kim-em
    kim-em committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    04524bc View commit details
    Browse the repository at this point in the history

Commits on Jan 15, 2024

  1. merge master and fix

    @kim-em
    kim-em committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    14bf968 View commit details
    Browse the repository at this point in the history

  2. add assert_not_exists

    @kim-em
    kim-em committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    78753aa View commit details
    Browse the repository at this point in the history

Commits on Jan 17, 2024

  1. delete Algebra.Group.Classes

    @YaelDillies
    YaelDillies committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    e7b2f74 View commit details
    Browse the repository at this point in the history

  2. delete unnecessary import

    @YaelDillies
    YaelDillies committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    1d45544 View commit details
    Browse the repository at this point in the history

  3. final cleanup

    @YaelDillies
    YaelDillies committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    0905b81 View commit details
    Browse the repository at this point in the history