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

Irrelevance of Prop WIP #875

Merged
merged 12 commits into from
Jan 7, 2023
Merged

Irrelevance of Prop WIP #875

merged 12 commits into from
Jan 7, 2023

Commits on Jan 6, 2023

  1. unify: irrelevance of Prop

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    57d4063 View commit details
    Browse the repository at this point in the history

  2. unify: improve irrelevance of Prop

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    38d4377 View commit details
    Browse the repository at this point in the history

  3. unify: substitute data type properly

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    a91bd13 View commit details
    Browse the repository at this point in the history

  4. conquer: use simpler interface

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    3f89c8f View commit details
    Browse the repository at this point in the history

  5. conquer: subst return type

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    c4e7b1d View commit details
    Browse the repository at this point in the history

  6. conquer: cleanup, improve unification getType

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    94b2f8b View commit details
    Browse the repository at this point in the history

  7. confluence: prepare for unify pat to produce a subst

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    5dfa3a0 View commit details
    Browse the repository at this point in the history

  8. refactor: introduce a standalone class for confluence check

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    60474a6 View commit details
    Browse the repository at this point in the history

  9. con: use correct selfTele, which is substituted by mischa

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    6fa8442 View commit details
    Browse the repository at this point in the history

  10. subst: linked

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    92be278 View commit details
    Browse the repository at this point in the history

  11. tests: add fixtures

    @ice1000
    ice1000 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    ef94733 View commit details
    Browse the repository at this point in the history

Commits on Jan 7, 2023

  1. subst: always use a linked map

    @ice1000
    ice1000 committed Jan 7, 2023
    Configuration menu
    Copy the full SHA
    7c01dac View commit details
    Browse the repository at this point in the history