Skip to content

Navigation Menu

Appearance settings

View all features
- BY COMPANY SIZE
  Enterprises
  Small and medium teams
  Startups
  Nonprofits
- BY USE CASE
  App Modernization
  DevSecOps
  DevOps
  CI/CD
  View all use cases
- BY INDUSTRY
  Healthcare
  Financial services
  Manufacturing
  Government
  View all industries
View all solutions
- EXPLORE BY TOPIC
  AI
  Software Development
  DevOps
  Security
  View all topics
- EXPLORE BY TYPE
  Customer stories
  Events & webinars
  Ebooks & reports
  Business insights
  GitHub Skills
- SUPPORT & SERVICES
  Documentation
  Customer support
  Community forum
  Trust center
  Partners
- COMMUNITY
  GitHub SponsorsFund open source developers
- PROGRAMS
  Security Lab
  Maintainer Community
  Accelerator
  Archive Program
- REPOSITORIES
  Topics
  Trending
  Collections
- ENTERPRISE SOLUTIONS
  Enterprise platformAI-powered developer platform
- AVAILABLE ADD-ONS
  GitHub Advanced SecurityEnterprise-grade security features
  Copilot for BusinessEnterprise-grade AI features
  Premium SupportEnterprise-grade 24/7 support
Pricing

Search code, repositories, users, issues, pull requests...

Search

Clear

Search syntax tips

Provide feedback

We read every piece of feedback, and take your input very seriously.

Include my email address so I can be contacted

Saved searches

Use saved searches to filter your results more quickly

Name

Query

To see all available qualifiers, see our documentation.

Appearance settings

You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session.

Dismiss alert

AeneasVerif / aeneas Public

Notifications You must be signed in to change notification settings
Fork 38
Star 474

Code
Issues 98
Pull requests 11
Actions
Projects
Security
Insights

Additional navigation options

Code
Issues
Pull requests
Actions
Projects
Security
Insights

Improve the performance of `condSimpTac`#558

Draft

sonmarcho wants to merge 31 commits intomainAeneasVerif/aeneas:mainfrom

son/scalar_tacAeneasVerif/aeneas:son/scalar_tacCopy head branch name to clipboard

Conversation Commits31 (31)Checks Files changed

Draft

Improve the performance of `condSimpTac`#558
sonmarcho wants to merge 31 commits intomainfrom
son/scalar_tac

Commits

Commits on Jun 20, 2025

Move the simp wrappers
sonmarcho
committed
Update the simp wrappers so that they output the updated fvar ids
sonmarcho
committed

Commits on Jun 23, 2025

Implement simpAllAssumptions
sonmarcho
committed
Start working on an incremental version of scalarTacPreprocess
sonmarcho
committed
Implement Simp.tacticToDischarge
sonmarcho
committed
Update condSimpTac to incrementally preprocess the goal
sonmarcho
committed
Fix an issue in ScalarTac.scalarTacPartialPreprocess
sonmarcho
committed
Use the isProp from the standard library
sonmarcho
committed
Do not unfold the local decls in the hyps to use in condSimpTac
sonmarcho
committed

Commits on Jun 24, 2025

Make a minor modification to scalar_decr_tac
sonmarcho
committed
Move some scalar_tac tests
sonmarcho
committed
Use specialized simp lemmas to simplify the hyps to use in condSimpTac
sonmarcho
committed
Fix a minor issue in the simpAll step of scalarTacPartialPreprocess
sonmarcho
committed
Make minor modifications
sonmarcho
committed
Add some scalar_tac lemmas
sonmarcho
committed
Add a simp_lists test
sonmarcho
committed
Simplify Int.cast_subNatNat in scalar_tac, simp_scalar, etc.
sonmarcho
committed
Cleanup a bit the simp_lists tests
sonmarcho
committed
Improve tracting in progress and progress* and improve progress*
sonmarcho
committed
Fix an issue in `progress`
sonmarcho
committed

Commits on Jun 25, 2025

Make progress* always try scalar_tac on the final goal
sonmarcho
committed
Marke the From....from_val_eq lemmas as `scalar_tac_simps`
sonmarcho
committed
Start cleaning up progress
sonmarcho
committed
Cleanup Progress further
sonmarcho
committed
Improve the tracing in saturate, scalarTac and condSimpTac
sonmarcho
committed
Make prettyMonadEq a Type rather than a Prop
sonmarcho
committed
Update the rule timed-lean in the Makefile
sonmarcho
committed

Commits on Jun 27, 2025

Add a state to progress
sonmarcho
committed
Use the state in progress*
sonmarcho
committed
Fix issues with ScalarTac.partialPreprocess
sonmarcho
committed
Fix an issue in partialPreprocess
sonmarcho
committed

Footer

© 2025 GitHub, Inc.

Footer navigation

Terms
Privacy
Security
Status
Community
Docs
Contact

You can’t perform that action at this time.