Search results

mlRewriteBy ... in ... suceeds, even if LHS doesn't appear in the hypothesis, but it appears in the goal.

Status: Open.

#449 In harp-project/AML-Formalization;

· Thrithralas opened on Jan 27, 2025

mlRewriteBy fails if goal matches LHS of =ml

Status: Open.

#448 In harp-project/AML-Formalization;

· Thrithralas opened on Jan 27, 2025

Prove proof constraint independence

enhancementEnhancement of existing featuresEnhancement of existing features

new featureAddition of new featuresAddition of new features

questionFurther information is requestedFurther information is requested

Status: Open.

#442 In harp-project/AML-Formalization;

· berpeti opened on Nov 12, 2024

Revise the axiom for definedness

bugSomething isn't workingSomething isn't working

good first issueGood for newcomersGood for newcomers

urgent

Status: Open.

#439 In harp-project/AML-Formalization;

· berpeti opened on Oct 2, 2024

Better notations

good first issueGood for newcomersGood for newcomers

questionFurther information is requestedFurther information is requested

student-friendlyGood tasks for master studentsGood tasks for master students

Status: Open.

#436 In harp-project/AML-Formalization;

· berpeti opened on Sep 6, 2024

Minor improvement ideas

good first issueGood for newcomersGood for newcomers

new featureAddition of new featuresAddition of new features

student-friendlyGood tasks for master studentsGood tasks for master students

Status: Open.

#433 In harp-project/AML-Formalization;

· berpeti opened on Aug 13, 2024

Investigate whether using context tactic to express proof mode tactics makes them more efficient (compared to computation)

enhancementEnhancement of existing featuresEnhancement of existing features

questionFurther information is requestedFurther information is requested

Status: Open.

#427 In harp-project/AML-Formalization;

· berpeti opened on Apr 11, 2024

mlSimpl enhancements

enhancementEnhancement of existing featuresEnhancement of existing features

Status: Open.

#426 In harp-project/AML-Formalization;

· berpeti opened on Mar 27, 2024

mlSpecialize and mlIntro should work for functional patterns and sorted quantifiers

enhancementEnhancement of existing featuresEnhancement of existing features

Status: Open.

#423 In harp-project/AML-Formalization;

· adilido99 opened on Jan 28, 2024

Utilize dependent pairs more

enhancementEnhancement of existing featuresEnhancement of existing features

new featureAddition of new featuresAddition of new features

Status: Open.

#422 In harp-project/AML-Formalization;

· Engreyight opened on Jan 16, 2024

Tactics should signal wrong ProofInfo

bugSomething isn't workingSomething isn't working

documentationImprovements or additions to documentationImprovements or additions to documentation

enhancementEnhancement of existing featuresEnhancement of existing features

Status: Open.

#421 In harp-project/AML-Formalization;

· Engreyight opened on Jan 16, 2024

Define the Peano induction in the Object level not in Meta level

new featureAddition of new featuresAddition of new features

Status: Open.

#418 In harp-project/AML-Formalization;

· adilido99 opened on Dec 10, 2023