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.Set.Intervals.Disjoint #1198

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: port Data.Set.Intervals.Disjoint #1198

wants to merge 12 commits into from

Commits on Dec 24, 2022

  1. Initial file copy from mathport

    @riccardobrasca
    riccardobrasca committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    91d413a View commit details
    Browse the repository at this point in the history

  2. Mathbin -> Mathlib; add import to Mathlib.lean

    @riccardobrasca
    riccardobrasca committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    a898571 View commit details
    Browse the repository at this point in the history

  3. fix this

    @riccardobrasca
    riccardobrasca committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    d09e732 View commit details
    Browse the repository at this point in the history

  4. this should compile

    @riccardobrasca
    riccardobrasca committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    625fbf3 View commit details
    Browse the repository at this point in the history

  5. fix doc

    @riccardobrasca
    riccardobrasca committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    9f443bf View commit details
    Browse the repository at this point in the history

  6. fix names

    @riccardobrasca
    riccardobrasca committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    2be01c9 View commit details
    Browse the repository at this point in the history

  7. long line

    @riccardobrasca
    riccardobrasca committed Dec 24, 2022
    Configuration menu
    Copy the full SHA
    1fed524 View commit details
    Browse the repository at this point in the history

Commits on Dec 26, 2022

  1. Update Mathlib/Data/Set/Intervals/Disjoint.lean 

    Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
    @riccardobrasca @dupuisf
    riccardobrasca and dupuisf committed Dec 26, 2022
    Configuration menu
    Copy the full SHA
    48ced31 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Data/Set/Intervals/Disjoint.lean 

    Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
    @riccardobrasca @dupuisf
    riccardobrasca and dupuisf committed Dec 26, 2022
    Configuration menu
    Copy the full SHA
    91d1f0d View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Data/Set/Intervals/Disjoint.lean 

    Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
    @riccardobrasca @dupuisf
    riccardobrasca and dupuisf committed Dec 26, 2022
    Configuration menu
    Copy the full SHA
    2d7d85f View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Data/Set/Intervals/Disjoint.lean 

    Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
    @riccardobrasca @dupuisf
    riccardobrasca and dupuisf committed Dec 26, 2022
    Configuration menu
    Copy the full SHA
    93d2d3b View commit details
    Browse the repository at this point in the history

  5. fix build

    @riccardobrasca
    riccardobrasca committed Dec 26, 2022
    Configuration menu
    Copy the full SHA
    5324259 View commit details
    Browse the repository at this point in the history