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 Geometry.Manifold.Instances.Sphere #5571

Closed
wants to merge 32 commits into from
Closed

[Merged by Bors] - feat: port Geometry.Manifold.Instances.Sphere #5571

wants to merge 32 commits into from

Commits on Jun 29, 2023

  1. feat: port Geometry.Manifold.Instances.Sphere

    @urkud
    urkud committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    30acadc View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @urkud
    urkud committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    e780a55 View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @urkud
    urkud committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    a08abc8 View commit details
    Browse the repository at this point in the history

  4. Snapshot

    @urkud
    urkud committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    8d33e91 View commit details
    Browse the repository at this point in the history

  5. Snapshot

    @urkud
    urkud committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    660f703 View commit details
    Browse the repository at this point in the history

  6. Snapshot

    @urkud
    urkud committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    c742456 View commit details
    Browse the repository at this point in the history

  7. Snapshot

    @urkud
    urkud committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    e18482a View commit details
    Browse the repository at this point in the history

  8. Update

    @urkud
    urkud committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    ebaa531 View commit details
    Browse the repository at this point in the history

  9. Update

    @urkud
    urkud committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    cedbc28 View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2023

  1. Merge branch 'master' into port/Geometry.Manifold.Instances.Sphere

    @urkud
    urkud committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    6e83749 View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2023

  1. Merge branch 'master' into port/Geometry.Manifold.Instances.Sphere

    @urkud
    urkud committed Jul 2, 2023
    Configuration menu
    Copy the full SHA
    ac595f7 View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2023

  1. Merge branch 'master' into port/Geometry.Manifold.Instances.Sphere

    @mattrobball
    mattrobball committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    4cdca35 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into port/Geometry.Manif… 

    …old.Instances.Sphere
    @urkud
    urkud committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    9c78968 View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2023

  1. Merge branch 'master' into port/Geometry.Manifold.Instances.Sphere

    @urkud
    urkud committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    fa82d8e View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'refs/remotes/origin/port/Geometry.Manif… 

    …old.Instances.Sphere' into port/Geometry.Manifold.Instances.Sphere
    @mattrobball
    mattrobball committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    183019e View commit details
    Browse the repository at this point in the history

  3. fix a few

    @mattrobball
    mattrobball committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    526dda9 View commit details
    Browse the repository at this point in the history

  4. fix some

    @mattrobball
    mattrobball committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    9b5cd91 View commit details
    Browse the repository at this point in the history

Commits on Jul 15, 2023

  1. fix more

    @mattrobball
    mattrobball committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    78aeec3 View commit details
    Browse the repository at this point in the history

  2. fix a little more

    @mattrobball
    mattrobball committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    da18d53 View commit details
    Browse the repository at this point in the history

  3. fix all but two

    @mattrobball
    mattrobball committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    d89b3d8 View commit details
    Browse the repository at this point in the history

  4. fix one error

    @hrmacbeth
    hrmacbeth committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    e1de9cd View commit details
    Browse the repository at this point in the history

  5. one more

    @hrmacbeth
    hrmacbeth committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    97b644a View commit details
    Browse the repository at this point in the history

  6. a little more

    @hrmacbeth
    hrmacbeth committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    2ef57fa View commit details
    Browse the repository at this point in the history

  7. one left

    @hrmacbeth
    hrmacbeth committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    f3c1935 View commit details
    Browse the repository at this point in the history

  8. lint and rename

    @mattrobball
    mattrobball committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    4c3b7e5 View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'refs/remotes/origin/port/Geometry.Manif… 

    …old.Instances.Sphere' into port/Geometry.Manifold.Instances.Sphere
    @mattrobball
    mattrobball committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    01510a0 View commit details
    Browse the repository at this point in the history

  10. rm new file

    @mattrobball
    mattrobball committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    d34b761 View commit details
    Browse the repository at this point in the history

  11. fixed

    @hrmacbeth
    hrmacbeth committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    2a463f1 View commit details
    Browse the repository at this point in the history

  12. Merge branch 'master' into port/Geometry.Manifold.Instances.Sphere

    @urkud
    urkud committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    c430132 View commit details
    Browse the repository at this point in the history

  13. fix

    @hrmacbeth
    hrmacbeth committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    6b00c0d View commit details
    Browse the repository at this point in the history

  14. Fix

    @urkud
    urkud committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    a8c7a29 View commit details
    Browse the repository at this point in the history

  15. Merge branch 'port/Geometry.Manifold.Instances.Sphere' of ssh://githu… 

    …b.com/leanprover-community/mathlib4 into port/Geometry.Manifold.Instances.Sphere
    @urkud
    urkud committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    36f68a4 View commit details
    Browse the repository at this point in the history