Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(data/multiset/sort): make multiset repr a meta instance #18163

Closed
wants to merge 20 commits into from
Closed

[Merged by Bors] - chore(data/multiset/sort): make multiset repr a meta instance #18163

wants to merge 20 commits into from

Commits on Jan 13, 2023

  1. chore(data/multiset/sort): make has_repr a meta instance to reduce im… 

    …ports
    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    b9b9140 View commit details
    Browse the repository at this point in the history

  2. fix build

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    21bd006 View commit details
    Browse the repository at this point in the history

  3. fix build

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    a418384 View commit details
    Browse the repository at this point in the history

  4. Update src/data/multiset/sort.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @ChrisHughes24 @eric-wieser
    ChrisHughes24 and eric-wieser authored Jan 13, 2023
    Configuration menu
    Copy the full SHA
    e218fdd View commit details
    Browse the repository at this point in the history

  5. Update src/data/pnat/factors.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @ChrisHughes24 @eric-wieser
    ChrisHughes24 and eric-wieser authored Jan 13, 2023
    Configuration menu
    Copy the full SHA
    38a0506 View commit details
    Browse the repository at this point in the history

  6. Update src/data/pnat/factors.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @ChrisHughes24 @eric-wieser
    ChrisHughes24 and eric-wieser authored Jan 13, 2023
    Configuration menu
    Copy the full SHA
    7b323f2 View commit details
    Browse the repository at this point in the history

  7. make the instance non-meta again

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    4c98928 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'multiset-repr-meta' of https://github.com/leanprover-co… 

    …mmunity/mathlib into multiset-repr-meta
    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    077459f View commit details
    Browse the repository at this point in the history

  9. revert changes to other files

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    60c1bd6 View commit details
    Browse the repository at this point in the history

  10. Revert "make the instance non-meta again" 

    This reverts commit 4c98928.
    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    afb48c2 View commit details
    Browse the repository at this point in the history

  11. meta instance

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    1c303e1 View commit details
    Browse the repository at this point in the history

  12. make finset instance meta

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    2c8201f View commit details
    Browse the repository at this point in the history

  13. fix factors

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    f0ef658 View commit details
    Browse the repository at this point in the history

  14. fix cycle.lean

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    a1f4b21 View commit details
    Browse the repository at this point in the history

  15. Update src/data/multiset/sort.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @ChrisHughes24 @eric-wieser
    ChrisHughes24 and eric-wieser authored Jan 13, 2023
    Configuration menu
    Copy the full SHA
    f9ada7d View commit details
    Browse the repository at this point in the history

  16. Update src/data/pnat/factors.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @ChrisHughes24 @eric-wieser
    ChrisHughes24 and eric-wieser authored Jan 13, 2023
    Configuration menu
    Copy the full SHA
    7ad390b View commit details
    Browse the repository at this point in the history

  17. fix

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    21358ee View commit details
    Browse the repository at this point in the history

  18. fix test

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    05db679 View commit details
    Browse the repository at this point in the history

  19. adjut test

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    a41d573 View commit details
    Browse the repository at this point in the history

  20. Update test/cycle.lean

    @eric-wieser
    eric-wieser authored Jan 13, 2023
    Configuration menu
    Copy the full SHA
    c221d9e View commit details
    Browse the repository at this point in the history