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: port Data.Real.CauSeqCompletion #1469

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat: port Data.Real.CauSeqCompletion #1469

wants to merge 5 commits into from

Commits on Jan 10, 2023

  1. Revert "Revert "feat: port Mathlib.Data.Real.CauSeqCompletion (#1440)" ( 

    #1468)"

This reverts commit 771dfd4.
    @eric-wieser
    eric-wieser committed Jan 10, 2023
    Configuration menu
    Copy the full SHA
    c0ee4cf View commit details
    Browse the repository at this point in the history

Commits on Jan 11, 2023

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/restore… 

    …-CauSeqCompletion
    @eric-wieser
    eric-wieser committed Jan 11, 2023
    Configuration menu
    Copy the full SHA
    e8ec3a0 View commit details
    Browse the repository at this point in the history

  2. apply fixes manually

    @eric-wieser
    eric-wieser committed Jan 11, 2023
    Configuration menu
    Copy the full SHA
    fe34ed5 View commit details
    Browse the repository at this point in the history

  3. adjust to match port output

    @eric-wieser
    eric-wieser committed Jan 11, 2023
    Configuration menu
    Copy the full SHA
    83f3234 View commit details
    Browse the repository at this point in the history

Commits on Jan 12, 2023

  1. fix

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    e839638 View commit details
    Browse the repository at this point in the history