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

Proof that reordering of constructors is correct #1095

Merged
merged 13 commits into from
Jul 22, 2024
Merged

Proof that reordering of constructors is correct #1095

merged 13 commits into from
Jul 22, 2024

Commits on Jul 12, 2024

  1. WIP on reordering constructors

    @mattam82
    mattam82 committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    39878e3 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2024

  1. New/old tag reasoning

    @mattam82
    mattam82 committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    1fa3d1d View commit details
    Browse the repository at this point in the history

  2. WIP correctness of constructor reordering. main lemma proven

    @mattam82
    mattam82 committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    adec8f4 View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2024

  1. Reordering preserves well-formedness

    @mattam82
    mattam82 committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    4a2c169 View commit details
    Browse the repository at this point in the history

  2. Reorderin

    @mattam82
    mattam82 committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    0a09b80 View commit details
    Browse the repository at this point in the history

  3. Admit free proofs of preservation for wf and substitution

    @mattam82
    mattam82 committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    d5297f4 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2024

  1. WIP adapting to an additional mapping argument for transforms and str… 

    …onger wellformedness property on extracted terms
    @mattam82
    mattam82 committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    9ecc7b5 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2024

  1. Full composed pipeline with mapping of constructors

    @mattam82
    mattam82 committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    75f368b View commit details
    Browse the repository at this point in the history

  2. Fixes due to removal of useless -fast flag and change for reordering … 

    …of constructors, now verified
    @mattam82
    mattam82 committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    2c201c5 View commit details
    Browse the repository at this point in the history

  3. Remove option to reorder constructors, now safely done always

    @mattam82
    mattam82 committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    67ee744 View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2024

  1. Fix metacoq_tour

    @mattam82
    mattam82 committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    c6180f0 View commit details
    Browse the repository at this point in the history

  2. Fix a remaining todo

    @mattam82
    mattam82 committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    b151425 View commit details
    Browse the repository at this point in the history

  3. Remove generated files

    @mattam82
    mattam82 committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    37d26b5 View commit details
    Browse the repository at this point in the history