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(slim_check): sampleable instance for generating functions and injective functions #3967

Closed
wants to merge 36 commits into from
Closed

[Merged by Bors] - feat(slim_check): sampleable instance for generating functions and injective functions #3967

wants to merge 36 commits into from

Commits on Sep 9, 2020

  1. feat(slim_check): subtype instances of sampleable

    @cipher1024
    cipher1024 committed Sep 9, 2020
    Configuration menu
    Copy the full SHA
    118ce3c View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2020

  1. fix build

    @cipher1024
    cipher1024 committed Sep 10, 2020
    Configuration menu
    Copy the full SHA
    98128ef View commit details
    Browse the repository at this point in the history

  2. fix lint warnings

    @cipher1024
    cipher1024 committed Sep 10, 2020
    Configuration menu
    Copy the full SHA
    571d812 View commit details
    Browse the repository at this point in the history

Commits on Sep 11, 2020

  1. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into slim-check-instances
    @cipher1024
    cipher1024 committed Sep 11, 2020
    Configuration menu
    Copy the full SHA
    aacc0db View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2020

  1. 1. add tracing option 2. allow gen expressions with #sample 3. de… 

    …fine `printable_prop`
    @cipher1024
    cipher1024 committed Sep 13, 2020
    Configuration menu
    Copy the full SHA
    acc9db4 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into slim-check-instances
    @cipher1024
    cipher1024 committed Sep 13, 2020
    Configuration menu
    Copy the full SHA
    ec8539d View commit details
    Browse the repository at this point in the history

  3. move test cases

    @cipher1024
    cipher1024 committed Sep 13, 2020
    Configuration menu
    Copy the full SHA
    6ac3de5 View commit details
    Browse the repository at this point in the history

  4. add function tests

    @cipher1024
    cipher1024 committed Sep 13, 2020
    Configuration menu
    Copy the full SHA
    8c80edd View commit details
    Browse the repository at this point in the history

  5. remove #check statements

    @cipher1024
    cipher1024 committed Sep 13, 2020
    Configuration menu
    Copy the full SHA
    b6ee0d8 View commit details
    Browse the repository at this point in the history

Commits on Sep 14, 2020

  1. Apply suggestions from code review 

    Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
    @cipher1024 @semorrison
    cipher1024 and semorrison committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    8901d68 View commit details
    Browse the repository at this point in the history

  2. shrink functions, add shrink tracing

    @cipher1024
    cipher1024 committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    61230c3 View commit details
    Browse the repository at this point in the history

  3. add module docs

    @cipher1024
    cipher1024 committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    aad55bd View commit details
    Browse the repository at this point in the history

  4. add simp attribute

    @cipher1024
    cipher1024 committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    92a90a3 View commit details
    Browse the repository at this point in the history

  5. add doc string to random instance and separate random and `bounde… 

    …d_random` classes
    @cipher1024
    cipher1024 committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    0062927 View commit details
    Browse the repository at this point in the history

  6. WIP: shrink injective functions

    @cipher1024
    cipher1024 committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    cfac72f View commit details
    Browse the repository at this point in the history

Commits on Sep 15, 2020

  1. WIP: shrink permutation

    @cipher1024
    cipher1024 committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    315435b View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into slim-check-instances
    @cipher1024
    cipher1024 committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    26aa72e View commit details
    Browse the repository at this point in the history

  3. shrink injective functions

    @cipher1024
    cipher1024 committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    ed7c657 View commit details
    Browse the repository at this point in the history

  4. Add shrinking information to error output

    @cipher1024
    cipher1024 committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    96facb4 View commit details
    Browse the repository at this point in the history

  5. move test case making script out of test file

    @cipher1024
    cipher1024 committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    5d75552 View commit details
    Browse the repository at this point in the history

  6. address lint issues

    @cipher1024
    cipher1024 committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    d1b4554 View commit details
    Browse the repository at this point in the history

  7. move lemmas and definitions to appropriate files

    @cipher1024
    cipher1024 committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    c275bd7 View commit details
    Browse the repository at this point in the history

  8. squeeze simp

    @cipher1024
    cipher1024 committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    daa6ee9 View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2020

  1. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into slim-check-instances
    @cipher1024
    cipher1024 committed Sep 16, 2020
    Configuration menu
    Copy the full SHA
    dedde02 View commit details
    Browse the repository at this point in the history

  2. address lint warnings

    @cipher1024
    cipher1024 committed Sep 16, 2020
    Configuration menu
    Copy the full SHA
    6575a49 View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2020

  1. Apply suggestions from code review 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @cipher1024 @bryangingechen
    cipher1024 and bryangingechen committed Sep 17, 2020
    Configuration menu
    Copy the full SHA
    17db2e5 View commit details
    Browse the repository at this point in the history

  2. Update functions.lean

    @cipher1024
    cipher1024 committed Sep 17, 2020
    Configuration menu
    Copy the full SHA
    29e320b View commit details
    Browse the repository at this point in the history

  3. Update slim_check.lean

    @cipher1024
    cipher1024 committed Sep 17, 2020
    Configuration menu
    Copy the full SHA
    d35dae5 View commit details
    Browse the repository at this point in the history

  4. move nth_injective

    @cipher1024
    cipher1024 committed Sep 17, 2020
    Configuration menu
    Copy the full SHA
    78c4f2a View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2020

  1. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into slim-check-instances
    @cipher1024
    cipher1024 committed Sep 24, 2020
    Configuration menu
    Copy the full SHA
    76eb507 View commit details
    Browse the repository at this point in the history

  2. Update src/data/list/basic.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @cipher1024 @bryangingechen
    cipher1024 and bryangingechen committed Sep 24, 2020
    Configuration menu
    Copy the full SHA
    79e3c47 View commit details
    Browse the repository at this point in the history

Commits on Sep 25, 2020

  1. document options

    @cipher1024
    cipher1024 committed Sep 25, 2020
    Configuration menu
    Copy the full SHA
    8f84a11 View commit details
    Browse the repository at this point in the history

  2. remove duplicate and tracing code

    @cipher1024
    cipher1024 committed Sep 25, 2020
    Configuration menu
    Copy the full SHA
    d22df65 View commit details
    Browse the repository at this point in the history

  3. use explicit variable naming in proof

    @cipher1024
    cipher1024 committed Sep 25, 2020
    Configuration menu
    Copy the full SHA
    85f3ccc View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2020

  1. comment on alists

    @cipher1024
    cipher1024 committed Oct 3, 2020
    Configuration menu
    Copy the full SHA
    07b7a9a View commit details
    Browse the repository at this point in the history

  2. explain sampleable_* classes in module doc

    @cipher1024
    cipher1024 committed Oct 3, 2020
    Configuration menu
    Copy the full SHA
    a4f3431 View commit details
    Browse the repository at this point in the history