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(data): port finsupp.ne_locus/lex to dfinsupp #16777

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat(data): port finsupp.ne_locus/lex to dfinsupp #16777

wants to merge 15 commits into from

Commits on Oct 1, 2022

  1. feat(data/pi/lex): generalize from partial_order to linear_order

    @alreadydone
    alreadydone committed Oct 1, 2022
    Configuration menu
    Copy the full SHA
    019c07e View commit details
    Browse the repository at this point in the history

  2. generalize in finsupp/lex

    @alreadydone
    alreadydone committed Oct 1, 2022
    Configuration menu
    Copy the full SHA
    6999897 View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2022

  1. port finsupp.ne_locus/lex to dfinsupp, preorder 

    lemmas, & use dfinsupp to golf finsupp
    @alreadydone
    alreadydone committed Oct 3, 2022
    Configuration menu
    Copy the full SHA
    ddd4652 View commit details
    Browse the repository at this point in the history

  2. omissions in finsupp->dfinsupp changes

    @alreadydone
    alreadydone committed Oct 3, 2022
    Configuration menu
    Copy the full SHA
    239386f View commit details
    Browse the repository at this point in the history

  3. copyright header

    @alreadydone
    alreadydone committed Oct 3, 2022
    Configuration menu
    Copy the full SHA
    00a51f3 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2022

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

    @alreadydone
    alreadydone committed Oct 4, 2022
    Configuration menu
    Copy the full SHA
    2c8b545 View commit details
    Browse the repository at this point in the history

  2. no need to name instance in lex.le_of_forall_le

    @alreadydone
    alreadydone committed Oct 4, 2022
    Configuration menu
    Copy the full SHA
    42234bc View commit details
    Browse the repository at this point in the history

  3. docstring fix

    @alreadydone
    alreadydone committed Oct 4, 2022
    Configuration menu
    Copy the full SHA
    1bf79cd View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2022

  1. golf + remove unnecessary naming of instance

    @alreadydone
    alreadydone committed Oct 5, 2022
    Configuration menu
    Copy the full SHA
    d8060ad View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2022

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

    @alreadydone
    alreadydone committed Oct 21, 2022
    Configuration menu
    Copy the full SHA
    f6e8929 View commit details
    Browse the repository at this point in the history

  2. match dfinsupp.ne_locus with finsupp

    @alreadydone
    alreadydone committed Oct 21, 2022
    Configuration menu
    Copy the full SHA
    3a3f2d0 View commit details
    Browse the repository at this point in the history

  3. fix

    @alreadydone
    alreadydone committed Oct 21, 2022
    Configuration menu
    Copy the full SHA
    979b1ba View commit details
    Browse the repository at this point in the history

  4. fix

    @alreadydone
    alreadydone committed Oct 21, 2022
    Configuration menu
    Copy the full SHA
    dd103cd View commit details
    Browse the repository at this point in the history

Commits on Oct 22, 2022

  1. remove lex.le_of_forall_le/le_of_of_lex_le

    @alreadydone
    alreadydone committed Oct 22, 2022
    Configuration menu
    Copy the full SHA
    1621bd7 View commit details
    Browse the repository at this point in the history

  2. fix

    @alreadydone
    alreadydone committed Oct 22, 2022
    Configuration menu
    Copy the full SHA
    01d507e View commit details
    Browse the repository at this point in the history