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(Data/List): Depend less on big operators #11741

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(Data/List): Depend less on big operators #11741

wants to merge 4 commits into from

Commits on Mar 28, 2024

  1. chore(Data/List): Depend less on big operators 

    * Make `Data.List.Count`, `Data.List.Dedup`, `Data.List.ProdSigma`, `Data.List.Range`, `Data.List.Rotate`, `Data.List.Zip` not depend on `Data.List.BigOperators.Basic`.
* As a consequence, move the big operators lemmas that were in there to `Data.List.BigOperators.Basic`. For the lemmas that were `Nat`-specific, keep a version of themin the original file but stated using `Nat.sum`.
* To help with this, add `Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum`.
    @YaelDillies
    YaelDillies committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    7d0d4de View commit details
    Browse the repository at this point in the history

  2. restore lost lemmas

    @YaelDillies
    YaelDillies committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    dde94dc View commit details
    Browse the repository at this point in the history

  3. shake

    @YaelDillies
    YaelDillies committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    0a4709f View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into list_no_big_ops

    @YaelDillies
    YaelDillies committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    4099508 View commit details
    Browse the repository at this point in the history