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

64 Open 33 Closed
64 Open 33 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

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
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
Adding new theorem new feature Addition of new features
#419 opened Dec 10, 2023 by adilido99
@berpeti
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
Extend mlSimpl to handle sorted quantification enhancement Enhancement of existing features
#407 opened Nov 13, 2023 by berpeti
1
Generalize mlRewriteBy with the new deduction theorem
#406 opened Nov 9, 2023 by berpeti
Precedence of =ml bug Something isn't working good first issue Good for newcomers student-friendly Good tasks for master students
#398 opened Oct 31, 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
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
Translation of nameless proofs to named proofs using proven alpha-renaming?
#362 opened Apr 28, 2023 by nishantjr
9
~Fix and~ extend ProofMode tutorial
#359 opened Apr 28, 2023 by h0nzZik
1
Search blacklist
#358 opened Apr 28, 2023 by h0nzZik
ProTip! Mix and match filters to narrow down what you’re looking for.