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: implement rpow norm_num extension #9893

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat: implement rpow norm_num extension #9893

wants to merge 14 commits into from

Commits on Jan 20, 2024

  1. feat: implement zpow norm_num extension

    @dwrensha
    dwrensha committed Jan 20, 2024
    Configuration menu
    Copy the full SHA
    058f917 View commit details
    Browse the repository at this point in the history

  2. hoist the haveI'

    @dwrensha
    dwrensha committed Jan 20, 2024
    Configuration menu
    Copy the full SHA
    4c065bb View commit details
    Browse the repository at this point in the history

  3. hoist it even higher

    @dwrensha
    dwrensha committed Jan 20, 2024
    Configuration menu
    Copy the full SHA
    ebd7dfa View commit details
    Browse the repository at this point in the history

Commits on Jan 21, 2024

  1. better style for .isRat wildcard match

    @dwrensha
    dwrensha committed Jan 21, 2024
    Configuration menu
    Copy the full SHA
    55b4a02 View commit details
    Browse the repository at this point in the history

  2. feat: add rpow norm_num extension

    @dwrensha
    dwrensha committed Jan 21, 2024
    Configuration menu
    Copy the full SHA
    c7ed7bc View commit details
    Browse the repository at this point in the history

  3. remove the long expresion

    @eric-wieser
    eric-wieser committed Jan 21, 2024
    Configuration menu
    Copy the full SHA
    aa06159 View commit details
    Browse the repository at this point in the history

  4. fix Bertrand.lean

    @dwrensha
    dwrensha committed Jan 21, 2024
    Configuration menu
    Copy the full SHA
    3a5c28a View commit details
    Browse the repository at this point in the history

  5. golf Qqs

    @eric-wieser
    eric-wieser committed Jan 21, 2024
    Configuration menu
    Copy the full SHA
    9661a15 View commit details
    Browse the repository at this point in the history

  6. add an assertion that the function is what we think it is

    @dwrensha
    dwrensha committed Jan 21, 2024
    Configuration menu
    Copy the full SHA
    0bc31f0 View commit details
    Browse the repository at this point in the history

Commits on Jan 22, 2024

  1. add .check

    @dwrensha
    dwrensha committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    344cc7a View commit details
    Browse the repository at this point in the history

  2. inline some positivity/norm_num1

    @dwrensha
    dwrensha committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    3763c5c View commit details
    Browse the repository at this point in the history

  3. inline e'

    @dwrensha
    dwrensha committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    33546e9 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into norm-num-rpow-2

    @dwrensha
    dwrensha committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    f2dae88 View commit details
    Browse the repository at this point in the history

  5. another inlining

    @dwrensha
    dwrensha committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    806af0c View commit details
    Browse the repository at this point in the history