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: existence of a limit in a concrete category implies smallness #11625

Closed
wants to merge 20 commits into from
Closed

[Merged by Bors] - feat: existence of a limit in a concrete category implies smallness #11625

wants to merge 20 commits into from

Commits on Mar 16, 2024

  1. replace TypeMax constructions by UnivLE assumptions

    @chrisflav
    chrisflav committed Mar 16, 2024
    Configuration menu
    Copy the full SHA
    abf1fed View commit details
    Browse the repository at this point in the history

  2. use inferInstanceAs everywhere

    @chrisflav
    chrisflav committed Mar 16, 2024
    Configuration menu
    Copy the full SHA
    7386ca7 View commit details
    Browse the repository at this point in the history

Commits on Mar 17, 2024

  1. Merge remote-tracking branch 'origin/master' into chrisflav/univle-mo… 

    …ncat.2
    @chrisflav
    chrisflav committed Mar 17, 2024
    Configuration menu
    Copy the full SHA
    109ea2b View commit details
    Browse the repository at this point in the history

Commits on Mar 22, 2024

  1. Merge remote-tracking branch 'origin/master' into chrisflav/univle-mo… 

    …ncat.2
    @chrisflav
    chrisflav committed Mar 22, 2024
    Configuration menu
    Copy the full SHA
    8d1b95f View commit details
    Browse the repository at this point in the history

Commits on Mar 23, 2024

  1. generalize to small sections

    @chrisflav
    chrisflav committed Mar 23, 2024
    Configuration menu
    Copy the full SHA
    66c1cfc View commit details
    Browse the repository at this point in the history

  2. fix trailing whitespace

    @chrisflav
    chrisflav committed Mar 23, 2024
    Configuration menu
    Copy the full SHA
    ab6ca39 View commit details
    Browse the repository at this point in the history

  3. change instances back to lemmas

    @chrisflav
    chrisflav committed Mar 23, 2024
    Configuration menu
    Copy the full SHA
    a565e5c View commit details
    Browse the repository at this point in the history

  4. remove standalone instances and inline instead

    @chrisflav
    chrisflav committed Mar 23, 2024
    Configuration menu
    Copy the full SHA
    85840b0 View commit details
    Browse the repository at this point in the history

  5. remove standalone instances and inline instead

    @chrisflav
    chrisflav committed Mar 23, 2024
    Configuration menu
    Copy the full SHA
    d88462d View commit details
    Browse the repository at this point in the history

Commits on Mar 24, 2024

  1. Merge remote-tracking branch 'origin/chrisflav/univle-moncat.2' into … 

    …forget-preserves-limits
    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    713845a View commit details
    Browse the repository at this point in the history

  2. feat: existence of a limit in a concrete category implies smallness

    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    7971356 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin' into forget-preserves-limits

    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    9ce848f View commit details
    Browse the repository at this point in the history

  4. fixing the build

    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    ff17df4 View commit details
    Browse the repository at this point in the history

  5. fixing the build

    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    ce270f0 View commit details
    Browse the repository at this point in the history

  6. fixing the build

    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    a924525 View commit details
    Browse the repository at this point in the history

  7. fixing the build

    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    bb3953e View commit details
    Browse the repository at this point in the history

  8. fixing the build

    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    ea67d66 View commit details
    Browse the repository at this point in the history

  9. fixing the build

    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    141d9ea View commit details
    Browse the repository at this point in the history

  10. added docstring

    @joelriou
    joelriou committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    930cae3 View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2024

  1. Merge remote-tracking branch 'origin' into forget-preserves-limits

    @joelriou
    joelriou committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    259d538 View commit details
    Browse the repository at this point in the history