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: @[inherit_doc] on notations #9942

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - doc: @[inherit_doc] on notations #9942

wants to merge 8 commits into from

Commits on Jan 23, 2024

  1. doc: @[inherit_doc] on notations 

    Make all the notations that unambiguously should inherit the docstring of their definition actually inherit it.

Also write a few docstrings by hand. I only wrote the ones I was competent to write and which I was sure of. Some docstrings come from mathlib3 as they were lost during the early port.

This PR is only intended as a first pass There are many more docstrings to add.
    @YaelDillies
    YaelDillies committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    053bbcf View commit details
    Browse the repository at this point in the history

  2. break long line

    @YaelDillies
    YaelDillies authored Jan 23, 2024
    Configuration menu
    Copy the full SHA
    d0c490b View commit details
    Browse the repository at this point in the history

  3. fix

    @YaelDillies
    YaelDillies committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    c0bbf78 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into notation_docs

    @YaelDillies
    YaelDillies committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    b02250b View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2024

  1. fix

    @YaelDillies
    YaelDillies committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    5035de8 View commit details
    Browse the repository at this point in the history

  2. fix

    @YaelDillies
    YaelDillies committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    4592d69 View commit details
    Browse the repository at this point in the history

Commits on Jan 30, 2024

  1. Merge remote-tracking branch 'origin/master' into notation_docs

    @YaelDillies
    YaelDillies committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    1791224 View commit details
    Browse the repository at this point in the history

  2. fix average docstrings

    @YaelDillies
    YaelDillies committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    50d502d View commit details
    Browse the repository at this point in the history