harp-project AML-Formalization issues

harp-project / AML-Formalization

GNU Lesser General Public License v2.1

10 stars 5 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

If a proof mode tactic can't solve a side condition, it shouldn't fail with an unhelpful message or hang forever

#443 Engreyight opened 1 week ago
0
Prove proof constraint independence

#442 berpeti opened 1 week ago
1
Extend `mlRewriteBy` notation

#441 Thrithralas closed 1 week ago
0
Simultaneous equality elimination for multiple equalities

#440 Engreyight closed 1 week ago
0
Revise the axiom for definedness

#439 berpeti opened 1 month ago
0
Exists singleton

#438 berpeti opened 1 month ago
0
Various improvements for substitution, equality elimination

#437 berpeti closed 2 months ago
0
Better notations

#436 berpeti opened 2 months ago
0
Proving application propagation lemma

#435 berpeti closed 2 months ago
0
Associativity of `$`

#434 berpeti closed 3 months ago
0
Minor improvement ideas

#433 berpeti opened 3 months ago
0
Remove unnecessary `Ensemble` imports and axiom usage in some modules

#432 berpeti closed 6 months ago
0
Unification

#431 Engreyight closed 3 months ago
1
Sum sort theory

#430 adilido99 closed 6 months ago
2
Product sort theory

#429 adilido99 closed 6 months ago
1
Default models for simple theories

#428 berpeti closed 7 months ago
0
Investigate whether using `context` tactic to express proof mode tactics makes them more efficient (compared to computation)

#427 berpeti opened 7 months ago
0
`mlSimpl` enhancements

#426 berpeti opened 8 months ago
0
Nat theory

#425 adilido99 closed 6 months ago
2
Update proofmode.md

#424 berpeti closed 9 months ago
0
`mlSpecialize` and `mlIntro` should work for functional patterns and sorted quantifiers

#423 adilido99 opened 10 months ago
0
Utilize dependent pairs more

#422 Engreyight opened 10 months ago
0
Tactics should signal wrong ProofInfo

#421 Engreyight opened 10 months ago
1
Improve `mlSortedSimpl`, theory extension theorem

#420 berpeti closed 11 months ago
0
Adding new theorem

#419 adilido99 closed 4 months ago
0
Define the Peano induction in the Object level not in Meta level

#418 adilido99 opened 11 months ago
0
Fix free set variable substitution and sorted binders

#417 adilido99 closed 11 months ago
0
Import again 5

#416 h0nzZik closed 11 months ago
0
Example OPML signatures and their extension

#415 h0nzZik closed 11 months ago
0
Signature morphisms; signature extension; invertors for model combinators

#414 h0nzZik closed 11 months ago
0
Generic OPML models

#413 h0nzZik closed 11 months ago
1
Bools theory

#412 adilido99 closed 11 months ago
0
Support Coq to 8.17 alongside 8.18

#411 h0nzZik closed 1 year ago
0
Generalize `mlRewrite` and `mlRewriteBy`

#410 berpeti opened 1 year ago
0
Various bugfixes

#409 berpeti closed 1 year ago
0
Generate signature from Kore

#408 h0nzZik closed 1 year ago
0
Extend `mlSimpl` to handle sorted quantification

#407 berpeti opened 1 year ago
1
Generalize `mlRewriteBy` with the new deduction theorem

#406 berpeti opened 1 year ago
0
Cleanup

#405 h0nzZik closed 1 year ago
0
Add `mlConj` with multiple parameters, improve rewrites

#404 berpeti closed 1 year ago
0
Pyk import

#403 h0nzZik closed 1 year ago
0
Kore import using Pyk 1 -- Sorts

#402 h0nzZik closed 1 year ago
0
Generalize `mlReflexivity` for all reflexive ML connectives

#401 berpeti closed 1 year ago
0
Example opml model: list of bools

#400 h0nzZik closed 1 year ago
0
Improve `mlReflexivity` to work on all reflexive operations

#399 berpeti closed 1 year ago
0
Precedence of `=ml`

#398 berpeti closed 3 months ago
1
`mlRewriteBy` fails for single-pattern goals

#397 berpeti closed 1 year ago
0
Better documentation of tactics

#396 berpeti closed 1 year ago
0
Create CI and proper documentation for opam usage

#395 berpeti opened 1 year ago
0
Bool syntax and upgrade to Coq 8.18.0

#394 berpeti closed 1 year ago
0