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

feat: dependent array type #813

Open
wants to merge 26 commits into
base: main
Choose a base branch
from
Open

feat: dependent array type #813

wants to merge 26 commits into from
+263 −0

Commits on May 27, 2024

  1. feat: dependent array type

    @fgdorais
    fgdorais committed May 27, 2024
    Configuration menu
    Copy the full SHA
    b98d7fa View commit details
    Browse the repository at this point in the history

  2. feat: experimental implementation

    @fgdorais
    fgdorais committed May 27, 2024
    Configuration menu
    Copy the full SHA
    0eca0e0 View commit details
    Browse the repository at this point in the history

  3. chore: docs and tests

    @fgdorais
    fgdorais committed May 27, 2024
    Configuration menu
    Copy the full SHA
    c632cf5 View commit details
    Browse the repository at this point in the history

  4. feat: use inductive model definition

    @fgdorais
    fgdorais committed May 27, 2024
    Configuration menu
    Copy the full SHA
    2e64898 View commit details
    Browse the repository at this point in the history

  5. chore: cleanup

    @fgdorais
    fgdorais committed May 27, 2024
    Configuration menu
    Copy the full SHA
    a59a726 View commit details
    Browse the repository at this point in the history

  6. chore: cleanup

    @fgdorais
    fgdorais committed May 27, 2024
    Configuration menu
    Copy the full SHA
    62a6444 View commit details
    Browse the repository at this point in the history

  7. chore: cleanup

    @fgdorais
    fgdorais committed May 27, 2024
    Configuration menu
    Copy the full SHA
    90a1e93 View commit details
    Browse the repository at this point in the history

Commits on May 28, 2024

  1. chore: more tests

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    c2ef604 View commit details
    Browse the repository at this point in the history

  2. fix: typos

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    e91f84c View commit details
    Browse the repository at this point in the history

  3. feat: add recOn and casesOn

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    8bd44e0 View commit details
    Browse the repository at this point in the history

  4. chore: cleanup and docs

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    ee049a5 View commit details
    Browse the repository at this point in the history

  5. chore: time for mk

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    45446e7 View commit details
    Browse the repository at this point in the history

  6. fix: docs

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    ddff5df View commit details
    Browse the repository at this point in the history

  7. feat: add Inhabited instance

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    419a4c4 View commit details
    Browse the repository at this point in the history

  8. chore: add todo for lean4#2292

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    88e32c9 View commit details
    Browse the repository at this point in the history

  9. fix: use NonScalar instead of Unit

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    11d3587 View commit details
    Browse the repository at this point in the history

  10. feat: add uget

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    bf511fd View commit details
    Browse the repository at this point in the history

  11. fix: remove recOn

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    f794ffa View commit details
    Browse the repository at this point in the history

  12. fix: typo

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    b581611 View commit details
    Browse the repository at this point in the history

  13. feat: add uset

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    3f815fe View commit details
    Browse the repository at this point in the history

  14. feat: add modify and umodify

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    10d0530 View commit details
    Browse the repository at this point in the history

  15. feat: add push and pop

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    c8d001c View commit details
    Browse the repository at this point in the history

  16. feat: lemmas for modify

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    332e74d View commit details
    Browse the repository at this point in the history

  17. fix: make modify and umodify semireducible

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    c665f52 View commit details
    Browse the repository at this point in the history

  18. chore: split Basic and Lemmas

    @fgdorais
    fgdorais committed May 28, 2024
    Configuration menu
    Copy the full SHA
    f25aaa8 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2024

  1. chore: merge main

    @fgdorais
    fgdorais committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    41c015d View commit details
    Browse the repository at this point in the history