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: classify porting notes about additional necessary beta reduction #12130

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - chore: classify porting notes about additional necessary beta reduction #12130

wants to merge 8 commits into from

Commits on Apr 13, 2024

  1. chore: classify porting notes about additional necessary beta reduction 

    I'm on the fence as to whether replacing the dsimp only by beta_reduce is useful, hence have split this into a separate commit.
    @grunweg
    grunweg committed Apr 13, 2024
    Configuration menu
    Copy the full SHA
    d820ab4 View commit details
    Browse the repository at this point in the history

  2. Change dsimp only to beta reduce; proof of concept.

    @grunweg
    grunweg committed Apr 13, 2024
    Configuration menu
    Copy the full SHA
    0d360d3 View commit details
    Browse the repository at this point in the history

  3. Some more; some porting notes are not quite true...

    @grunweg
    grunweg committed Apr 13, 2024
    Configuration menu
    Copy the full SHA
    2b6865a View commit details
    Browse the repository at this point in the history

  4. More instances. Decided to change them to beta_reduce at the same time. 

    Some of these notes were not true, and the best way to make them not regress
is to just do beta reduction.

This includes all remaining instances of 10971.
    @grunweg
    grunweg committed Apr 13, 2024
    Configuration menu
    Copy the full SHA
    9c35acc View commit details
    Browse the repository at this point in the history

  5. Last one; remove one superfluous simp only.

    @grunweg
    grunweg committed Apr 13, 2024
    Configuration menu
    Copy the full SHA
    000e11d View commit details
    Browse the repository at this point in the history

  6. A few more instances.

    @grunweg
    grunweg committed Apr 13, 2024
    Configuration menu
    Copy the full SHA
    a9e882a View commit details
    Browse the repository at this point in the history

Commits on Apr 14, 2024

  1. Filed BBBBB as 12129 now.

    @grunweg
    grunweg committed Apr 14, 2024
    Configuration menu
    Copy the full SHA
    54d5c10 View commit details
    Browse the repository at this point in the history

  2. Re-label the TODO notes.

    @grunweg
    grunweg committed Apr 14, 2024
    Configuration menu
    Copy the full SHA
    e84e789 View commit details
    Browse the repository at this point in the history