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

Lift implications laws #459

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

Lift implications laws #459

wants to merge 16 commits into from

Commits on Oct 9, 2024

  1. Add meta code to generate the theorems about laws (typechecks, but un… 

    …tested)
    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    f159b7c View commit details
    Browse the repository at this point in the history

  2. Split examples of FactSyntax, remove unnecessary dependency in FreeMagma

    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    3daabef View commit details
    Browse the repository at this point in the history

  3. update: theorem generation still not working

    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    924bcdd View commit details
    Browse the repository at this point in the history

  4. Split examples of FactSyntax, remove unnecessary dependency in FreeMagma

    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    37b9aa3 View commit details
    Browse the repository at this point in the history

  5. some improvements in meta code, but it still doesn't quite work (univ… 

    …erse issues?)
    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    66ecf66 View commit details
    Browse the repository at this point in the history

  6. Move Equation953 to Equations from AllEquations, as it is used in sub… 

    …graph
    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    c766887 View commit details
    Browse the repository at this point in the history

  7. move equation 953 from AllEquations to Equations, as it is used in Su… 

    …bgraph
    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    e5447f3 View commit details
    Browse the repository at this point in the history

  8. Revert "Move Equation953 to Equations from AllEquations, as it is use… 

    …d in subgraph"

This reverts commit c766887.
    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    d1cfd79 View commit details
    Browse the repository at this point in the history

  9. term is type correct but not considered defeq

    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    d36b2a0 View commit details
    Browse the repository at this point in the history

  10. it works!

    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    963de11 View commit details
    Browse the repository at this point in the history

  11. Merge remote-tracking branch 'origin' into cleanup-magmalaw-factsyntax

    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    c5ca953 View commit details
    Browse the repository at this point in the history

  12. Merge branch 'cleanup-magmalaw-factsyntax' into lift_implications_laws

    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    b577572 View commit details
    Browse the repository at this point in the history

  13. don't try to build implications if equational result is not an implic… 

    …ation
    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    d73c2e3 View commit details
    Browse the repository at this point in the history

  14. Merge remote-tracking branch 'origin/main' into lift_implications_laws

    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    9f50628 View commit details
    Browse the repository at this point in the history

  15. fix dangling abrev

    @goens
    goens committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    bd53f87 View commit details
    Browse the repository at this point in the history

Commits on Oct 10, 2024

  1. Merge branch 'main' into lift_implications_laws

    @pitmonticone
    pitmonticone authored Oct 10, 2024
    Configuration menu
    Copy the full SHA
    aa71a17 View commit details
    Browse the repository at this point in the history