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

Smallness #1867

Merged
merged 47 commits into from
Sep 24, 2024
Merged

Smallness #1867

merged 47 commits into from
Sep 24, 2024

Commits on Feb 19, 2024

  1. Smallness 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    8a786e7 View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2024

  1. Merge branch 'master' into ps/branch/smallness

    @Alizter
    Alizter authored Sep 21, 2024
    Configuration menu
    Copy the full SHA
    e839d96 View commit details
    Browse the repository at this point in the history

  2. move ObjectClassifier.v to Universes/ 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    dd88db7 View commit details
    Browse the repository at this point in the history

  3. move DProp.v to Universes/ 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    bc23ce5 View commit details
    Browse the repository at this point in the history

  4. move HProp.v to Universes/ 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    446abbc View commit details
    Browse the repository at this point in the history

  5. move HSet.v to Universes/ 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    1361729 View commit details
    Browse the repository at this point in the history

  6. move UniverseLevel.v to Universes/ 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    2cf1be3 View commit details
    Browse the repository at this point in the history

  7. move TruncType.v to Universes 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    ade8699 View commit details
    Browse the repository at this point in the history

  8. STYLE.md: update to reflect new Universes/ folder

    @jdchristensen
    jdchristensen committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    c6cd3d4 View commit details
    Browse the repository at this point in the history

Commits on Sep 22, 2024

  1. Merge branch 'master' into ps/branch/smallness

    @Alizter
    Alizter authored Sep 22, 2024
    Configuration menu
    Copy the full SHA
    9e2c076 View commit details
    Browse the repository at this point in the history

  2. use smallness in PropResizing 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    c79bebf View commit details
    Browse the repository at this point in the history

  3. make IsSmall cumulative 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    17a2823 View commit details
    Browse the repository at this point in the history

  4. fit things in margin 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    a32acae View commit details
    Browse the repository at this point in the history

  5. reformat record 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    83cf95d View commit details
    Browse the repository at this point in the history

  6. move homeless lemmas from Smallness to PropResizing 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    0bf9633 View commit details
    Browse the repository at this point in the history

  7. remove stale comments 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    194ac26 View commit details
    Browse the repository at this point in the history

  8. move Smallness.v to Universes 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    6118f28 View commit details
    Browse the repository at this point in the history

  9. Smallness, PropResizing: use "islocallysmall" and "issmall" consistently

    @jdchristensen
    jdchristensen committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    067631b View commit details
    Browse the repository at this point in the history

  10. PropResizing: clarify comment about universes, now that we have cumul… 

    …ativity
    @jdchristensen
    jdchristensen committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    dd53e48 View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2024

  1. move IsSmall to Overture.v 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    82d6460 View commit details
    Browse the repository at this point in the history

  2. move extra prop resizing lemmas back to Smallness.v 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    7e80dc0 View commit details
    Browse the repository at this point in the history

  3. refine imports for PropResizing 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    1af5422 View commit details
    Browse the repository at this point in the history

  4. add todos for Smallness.v 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    13cf546 View commit details
    Browse the repository at this point in the history

  5. fix order of universe vars 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    9fa3101 View commit details
    Browse the repository at this point in the history

  6. remove todos from PropResizing about inlining 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    12fd26a View commit details
    Browse the repository at this point in the history

  7. move trunc_index_to_nat and refine requires 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    f817791 View commit details
    Browse the repository at this point in the history

  8. make IsSmall a typeclass 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    f6af27f View commit details
    Browse the repository at this point in the history

  9. remove equiv_resize_hprop 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    ad8e561 View commit details
    Browse the repository at this point in the history

  10. remove resize_hprop and replace with smalltype 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    f8778c0 View commit details
    Browse the repository at this point in the history

  11. remove ishprop_resize_hprop 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    824e536 View commit details
    Browse the repository at this point in the history

  12. inline PropResizing.v in Overture.v 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    9eb3553 View commit details
    Browse the repository at this point in the history

  13. update comments add instances 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    fb82214 View commit details
    Browse the repository at this point in the history

  14. update STYLE.md 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    3ff42f4 View commit details
    Browse the repository at this point in the history

  15. clarify Smallness require 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    2ec2f24 View commit details
    Browse the repository at this point in the history

  16. STYLE.md: fix typo

    @jdchristensen
    jdchristensen authored Sep 23, 2024
    Configuration menu
    Copy the full SHA
    7f93879 View commit details
    Browse the repository at this point in the history

  17. make IsLocallySmall a typeclass 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    877d213 View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2024

  1. move PropResizing/ contents to Metatheory/ 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    291a203 View commit details
    Browse the repository at this point in the history

  2. include PropResizing axiom 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    151ae53 View commit details
    Browse the repository at this point in the history

  3. move Spaces/Universe.v to Universes/ 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    96d178b View commit details
    Browse the repository at this point in the history

  4. move BAut.v to Universes/ 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    4c16049 View commit details
    Browse the repository at this point in the history

  5. rename Universes.Universe -> Universes.Automorphisms 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    4e37926 View commit details
    Browse the repository at this point in the history

  6. move BAut/Rigid.v to Universes/ 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    872aae3 View commit details
    Browse the repository at this point in the history

  7. STYLE.md: update to match current situation

    @jdchristensen
    jdchristensen committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    3a6190e View commit details
    Browse the repository at this point in the history

  8. Types/Equiv, Smallness: minor cleanups

    @jdchristensen
    jdchristensen committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    92483c1 View commit details
    Browse the repository at this point in the history

  9. fix universe variance in IsSmall 

    Signed-off-by: Ali Caglayan <[email protected]>
    @Alizter
    Alizter committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    18c6a48 View commit details
    Browse the repository at this point in the history

  10. Revert "fix universe variance in IsSmall" 

    This reverts commit 18c6a48.
    @Alizter
    Alizter committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    9941271 View commit details
    Browse the repository at this point in the history

  11. Make universe i invariant in IsSmall; simplify lots elsewhere

    @jdchristensen
    jdchristensen committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    0011284 View commit details
    Browse the repository at this point in the history