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

refactor(*): saturating fin addition #6149

Closed
wants to merge 30 commits into from
Closed

refactor(*): saturating fin addition #6149

wants to merge 30 commits into from

Commits on Feb 8, 2021

  1. refactor(data/fin): convert fin to saturating add

    @pechersky
    pechersky committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    b487f72 View commit details
    Browse the repository at this point in the history

  2. chore(data/fin): reorder file to group declarations

    @pechersky
    pechersky committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    0422730 View commit details
    Browse the repository at this point in the history

  3. section titles

    @pechersky
    pechersky committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    e5372d9 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/pechersky/fin-refactor-reorder' … 

    …into fin-saturate-dev
    @pechersky
    pechersky committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    729e714 View commit details
    Browse the repository at this point in the history

Commits on Feb 9, 2021

  1. remove mul, add to min instead of mod

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    8b94d4a View commit details
    Browse the repository at this point in the history

  2. amend norm_fin tests

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    dccaeaf View commit details
    Browse the repository at this point in the history

  3. add of_nat' simplifying lemma

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    b7a093c View commit details
    Browse the repository at this point in the history

  4. make bitvec/basic compile

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    b0d6470 View commit details
    Browse the repository at this point in the history

  5. docstring for of_nat_eq

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    0521967 View commit details
    Browse the repository at this point in the history

  6. coe_coe_le_self

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    911b27b View commit details
    Browse the repository at this point in the history

  7. fix sampleable

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    047a6aa View commit details
    Browse the repository at this point in the history

  8. chore(group_theory/perm/sign): speed up sign_aux_swap_zero_one proof

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    2f61fe2 View commit details
    Browse the repository at this point in the history

  9. satisfy line length linter

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    fe5d98d View commit details
    Browse the repository at this point in the history

  10. Merge remote-tracking branch 'origin/pechersky/swap-aux-speedup' into… 

    … fin-saturate-dev
    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    9fe39ba View commit details
    Browse the repository at this point in the history

  11. fix sign

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    530df77 View commit details
    Browse the repository at this point in the history

  12. golf sign

    @pechersky
    pechersky committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    ba72663 View commit details
    Browse the repository at this point in the history

Commits on Feb 10, 2021

  1. fix notation

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    6941b7c View commit details
    Browse the repository at this point in the history

  2. attempt to fix zmod

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    af49782 View commit details
    Browse the repository at this point in the history

  3. feat(algebra/ordered_monoid): min_*_distrib

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    2badd53 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/pechersky/nat-canonical-linear-a… 

    …dd-monoid' into fin-saturate-dev
    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    71d8f72 View commit details
    Browse the repository at this point in the history

  5. feat(data/nat/basic): le_of_add_le_*

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    b2fb534 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/pechersky/le-of-add' into fin-sa… 

    …turate-dev
    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    f481443 View commit details
    Browse the repository at this point in the history

  7. remove now pr'd lemmas

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    18ccb4b View commit details
    Browse the repository at this point in the history

  8. fix ite lemmas in sign

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    c4d3477 View commit details
    Browse the repository at this point in the history

  9. remove noisy suggest

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    f8879d3 View commit details
    Browse the repository at this point in the history

  10. fix linear_recurrence

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    0ad2770 View commit details
    Browse the repository at this point in the history

  11. fix composition

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    e5ff12c View commit details
    Browse the repository at this point in the history

  12. fix circumcenter

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    25c2cda View commit details
    Browse the repository at this point in the history

  13. remove raise reference

    @pechersky
    pechersky committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    9e5e2f0 View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2021

  1. initial notation fix, gets some tests working

    @pechersky
    pechersky committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    48b74d7 View commit details
    Browse the repository at this point in the history