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

META: Automatically generate laws from equations together with proofs of equi-satisiability #428

Closed
0art0 opened this issue Oct 8, 2024 · 2 comments
Closed

META: Automatically generate laws from equations together with proofs of equi-satisiability #428

0art0 opened this issue Oct 8, 2024 · 2 comments
Assignees
@0art0
Labels
project-task

Comments

@0art0
Copy link
Contributor

0art0 commented Oct 8, 2024

The equation command that is used to define equations can also be modified to

  • automatically generate the corresponding law (with variables coming from Nat or Fin n)
  • automatically generate a proof that the law is equivalent to the original equation in terms of satisfiability
  • automatically register the law in a global environment extension to make the full list of laws available in other files

The PR #427 currently implements these features, and I can claim this issue and propose the PR as a solution once this issue gets promoted to a task.
@github-project-automation github-project-automation bot moved this to Unclaimed Outstanding Tasks in Equational Theories Project Oct 8, 2024
@0art0
Copy link
Contributor Author

0art0 commented Oct 8, 2024

claim

@teorth teorth moved this from Unclaimed Outstanding Tasks to Claimed Tasks in Equational Theories Project Oct 8, 2024
@0art0
Copy link
Contributor Author

0art0 commented Oct 8, 2024

propose PR #427

@teorth teorth moved this from Claimed Tasks to In Progress in Equational Theories Project Oct 8, 2024
@0art0 0art0 mentioned this issue Oct 8, 2024
Merged
@teorth teorth closed this as completed Oct 13, 2024
@github-project-automation github-project-automation bot moved this from In Progress to Completed Tasks in Equational Theories Project Oct 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@0art0 0art0

Labels
project-task
Projects
Equational Theories Project
Status: Completed Tasks
Milestone
No milestone
Development

No branches or pull requests
2 participants
@teorth @0art0