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] - doc(data/stream/defs): add docstrings to most defs #10547

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - doc(data/stream/defs): add docstrings to most defs #10547

wants to merge 12 commits into from

Commits on Nov 24, 2021

  1. chore(data/stream): move most defs to a new file

    @urkud
    urkud committed Nov 24, 2021
    Configuration menu
    Copy the full SHA
    832ad20 View commit details
    Browse the repository at this point in the history

  2. Snapshot

    @urkud
    urkud committed Nov 24, 2021
    Configuration menu
    Copy the full SHA
    c6e51c3 View commit details
    Browse the repository at this point in the history

  3. Add docs, remove @[reducible]

    @urkud
    urkud committed Nov 24, 2021
    Configuration menu
    Copy the full SHA
    4bcf076 View commit details
    Browse the repository at this point in the history

  4. Fix lint

    @urkud
    urkud committed Nov 24, 2021
    Configuration menu
    Copy the full SHA
    ce99a21 View commit details
    Browse the repository at this point in the history

Commits on Nov 28, 2021

  1. Merge branch 'master' into YK-stream-defs

    @urkud
    urkud committed Nov 28, 2021
    Configuration menu
    Copy the full SHA
    d70d7e8 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'YK-stream-defs' into YK-stream-take

    @urkud
    urkud committed Nov 28, 2021
    Configuration menu
    Copy the full SHA
    be190cc View commit details
    Browse the repository at this point in the history

  3. chore(data/stream): move 1 def, reduce imports

    @urkud
    urkud committed Nov 28, 2021
    Configuration menu
    Copy the full SHA
    0013ef5 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'YK-stream-import' into YK-stream-docs

    @urkud
    urkud committed Nov 28, 2021
    Configuration menu
    Copy the full SHA
    cfac659 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into YK-stream-take

    @urkud
    urkud committed Nov 28, 2021
    Configuration menu
    Copy the full SHA
    1e6189a View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2021

  1. Merge branch 'master' into YK-stream-take

    @urkud
    urkud committed Nov 30, 2021
    Configuration menu
    Copy the full SHA
    94c5c6f View commit details
    Browse the repository at this point in the history

  2. Merge branch 'YK-stream-take' into YK-stream-docs

    @urkud
    urkud committed Nov 30, 2021
    Configuration menu
    Copy the full SHA
    f16036b View commit details
    Browse the repository at this point in the history

  3. Update src/data/stream/defs.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @urkud @jcommelin
    urkud and jcommelin committed Nov 30, 2021
    Configuration menu
    Copy the full SHA
    aef32e9 View commit details
    Browse the repository at this point in the history