Skip to content

Issues: harp-project/AML-Formalization

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

66 Open 39 Closed
66 Open 39 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

mlRewriteBy ... in ... suceeds, even if LHS doesn't appear in the hypothesis, but it appears in the goal.
#449 opened Jan 27, 2025 by Thrithralas
mlRewriteBy fails if goal matches LHS of =ml
#448 opened Jan 27, 2025 by Thrithralas
Prove proof constraint independence enhancement Enhancement of existing features new feature Addition of new features question Further information is requested
#442 opened Nov 12, 2024 by berpeti
1
Revise the axiom for definedness bug Something isn't working good first issue Good for newcomers urgent
#439 opened Oct 2, 2024 by berpeti
Better notations good first issue Good for newcomers question Further information is requested student-friendly Good tasks for master students
#436 opened Sep 6, 2024 by berpeti
1
Minor improvement ideas good first issue Good for newcomers new feature Addition of new features student-friendly Good tasks for master students
#433 opened Aug 13, 2024 by berpeti
3 tasks
Investigate whether using context tactic to express proof mode tactics makes them more efficient (compared to computation) enhancement Enhancement of existing features question Further information is requested
#427 opened Apr 11, 2024 by berpeti
mlSimpl enhancements enhancement Enhancement of existing features
#426 opened Mar 27, 2024 by berpeti
@berpeti
mlSpecialize and mlIntro should work for functional patterns and sorted quantifiers enhancement Enhancement of existing features
#423 opened Jan 28, 2024 by adilido99
Utilize dependent pairs more enhancement Enhancement of existing features new feature Addition of new features
#422 opened Jan 16, 2024 by Engreyight
Tactics should signal wrong ProofInfo bug Something isn't working documentation Improvements or additions to documentation enhancement Enhancement of existing features
#421 opened Jan 16, 2024 by Engreyight
1
Define the Peano induction in the Object level not in Meta level new feature Addition of new features
#418 opened Dec 10, 2023 by adilido99
@berpeti
Generalize mlRewrite and mlRewriteBy bug Something isn't working enhancement Enhancement of existing features
#410 opened Nov 16, 2023 by berpeti
Generalize mlRewriteBy with the new deduction theorem
#406 opened Nov 9, 2023 by berpeti
Create CI and proper documentation for opam usage documentation Improvements or additions to documentation enhancement Enhancement of existing features
#395 opened Oct 24, 2023 by berpeti
Use intropatterns for mlIntros enhancement Enhancement of existing features
#387 opened Sep 28, 2023 by berpeti
Basic version of mlIntros in Ltac2 good first issue Good for newcomers new feature Addition of new features
#386 opened Sep 28, 2023 by berpeti
mlTransitivity tactic enhancement Enhancement of existing features good first issue Good for newcomers new feature Addition of new features
#384 opened Sep 26, 2023 by berpeti
1
Translation from Kore via OPML (order sorted matching mu-logic) to AML
#383 opened Sep 26, 2023 by berpeti
3 of 13 tasks
4
Integrate with an SMT Solver
#375 opened Jun 28, 2023 by h0nzZik
1
Proof mode tactics (based on _failIfUsed) do not work when StringMLVariables is used bug Something isn't working
#370 opened May 22, 2023 by berpeti
1
Elimination of substitutions new feature Addition of new features
#368 opened May 16, 2023 by berpeti
Proof mode tactics with and without the freshness manager enhancement Enhancement of existing features
#366 opened May 5, 2023 by berpeti
Freshness manager optimization enhancement Enhancement of existing features
#365 opened May 5, 2023 by berpeti
Freshness manager synchronization enhancement Enhancement of existing features
#364 opened May 5, 2023 by berpeti
1
ProTip! Find all open issues with in progress development work with linked:pr.