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] - perf(FunLike.Basic): beta reduce CoeFun.coe #7905

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - perf(FunLike.Basic): beta reduce CoeFun.coe #7905

wants to merge 28 commits into from

Commits on Oct 24, 2023

  1. chore: short cut instance for non-dependent FunLike 

    This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`.

Not sure about the name.
    @FR-vdash-bot
    FR-vdash-bot committed Oct 24, 2023
    Configuration menu
    Copy the full SHA
    67a8504 View commit details
    Browse the repository at this point in the history

  2. fix

    @FR-vdash-bot
    FR-vdash-bot committed Oct 24, 2023
    Configuration menu
    Copy the full SHA
    ec8fbfe View commit details
    Browse the repository at this point in the history

  3. fix

    @FR-vdash-bot
    FR-vdash-bot committed Oct 24, 2023
    Configuration menu
    Copy the full SHA
    1db1016 View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2023

  1. fix

    @FR-vdash-bot
    FR-vdash-bot committed Oct 25, 2023
    Configuration menu
    Copy the full SHA
    1d7a1cf View commit details
    Browse the repository at this point in the history

  2. fix

    @FR-vdash-bot
    FR-vdash-bot committed Oct 25, 2023
    Configuration menu
    Copy the full SHA
    d45d7ab View commit details
    Browse the repository at this point in the history

  3. fix

    @FR-vdash-bot
    FR-vdash-bot committed Oct 25, 2023
    Configuration menu
    Copy the full SHA
    2170722 View commit details
    Browse the repository at this point in the history

  4. fix

    @FR-vdash-bot
    FR-vdash-bot committed Oct 25, 2023
    Configuration menu
    Copy the full SHA
    d9b0cee View commit details
    Browse the repository at this point in the history

  5. fix

    @FR-vdash-bot
    FR-vdash-bot committed Oct 25, 2023
    Configuration menu
    Copy the full SHA
    2e8d234 View commit details
    Browse the repository at this point in the history

  6. fix

    @FR-vdash-bot
    FR-vdash-bot committed Oct 25, 2023
    Configuration menu
    Copy the full SHA
    f4a4e79 View commit details
    Browse the repository at this point in the history

Commits on Oct 26, 2023

  1. lint

    @FR-vdash-bot
    FR-vdash-bot committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    1dc6a94 View commit details
    Browse the repository at this point in the history

  2. fix

    @FR-vdash-bot
    FR-vdash-bot committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    4d6319b View commit details
    Browse the repository at this point in the history

  3. local high priority

    @FR-vdash-bot
    FR-vdash-bot committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    18d65c8 View commit details
    Browse the repository at this point in the history

  4. this is faster

    @FR-vdash-bot
    FR-vdash-bot committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    3414e9b View commit details
    Browse the repository at this point in the history

  5. docs

    @FR-vdash-bot
    FR-vdash-bot committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    1018451 View commit details
    Browse the repository at this point in the history

  6. suggestions

    @FR-vdash-bot
    FR-vdash-bot committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    176dadf View commit details
    Browse the repository at this point in the history

Commits on Nov 2, 2023

  1. Merge branch 'master' into FR_funlike_shortcut

    @mattrobball
    mattrobball committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    3e44aca View commit details
    Browse the repository at this point in the history

  2. fix

    @mattrobball
    mattrobball committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    8e4680c View commit details
    Browse the repository at this point in the history

Commits on Nov 15, 2023

  1. suggestions

    @FR-vdash-bot
    FR-vdash-bot committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    be37902 View commit details
    Browse the repository at this point in the history

  2. fix

    @FR-vdash-bot
    FR-vdash-bot committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    770cf0c View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into FR_funlike_shortcut

    @FR-vdash-bot
    FR-vdash-bot committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    ee13762 View commit details
    Browse the repository at this point in the history

  4. fix

    @FR-vdash-bot
    FR-vdash-bot committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    05cf3f6 View commit details
    Browse the repository at this point in the history

  5. fix

    @FR-vdash-bot
    FR-vdash-bot committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    4752f1c View commit details
    Browse the repository at this point in the history

  6. reduce diffs

    @FR-vdash-bot
    FR-vdash-bot committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    40912e7 View commit details
    Browse the repository at this point in the history

  7. keep both versions

    @FR-vdash-bot
    FR-vdash-bot committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    6267d0a View commit details
    Browse the repository at this point in the history

  8. suggestions

    @FR-vdash-bot
    FR-vdash-bot committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    b1bebb1 View commit details
    Browse the repository at this point in the history

  9. more notes

    @FR-vdash-bot
    FR-vdash-bot committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    bd9dd94 View commit details
    Browse the repository at this point in the history

  10. fix a weird rfl failure

    @eric-wieser
    eric-wieser committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    2b7a1d5 View commit details
    Browse the repository at this point in the history

  11. add comments

    @eric-wieser
    eric-wieser committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    73fdc27 View commit details
    Browse the repository at this point in the history