Skip to content
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.

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

feat: progress? to say which theorem has been used #277

Merged
merged 2 commits into from
Jul 5, 2024

Conversation

RaitoBezarius
Copy link
Contributor

@RaitoBezarius RaitoBezarius commented Jul 1, 2024

Like simp? and similar, progress? will provide what theorem was used to make the goal progress.

TODO:

  • grab original stx elements
  • show progress ... instead of ... during the print.
  • make code action work on this fragment

@RaitoBezarius RaitoBezarius force-pushed the progress-says branch 3 times, most recently from 6c63999 to d12d92d Compare July 2, 2024 14:02
@RaitoBezarius RaitoBezarius marked this pull request as ready for review July 2, 2024 14:03
Copy link
Member

@sonmarcho sonmarcho left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good! I have a minor suggestion, but this put aside you're good to merge :)

backends/lean/Base/Progress/Progress.lean Outdated Show resolved Hide resolved
Like `simp?` and similar, `progress?` will provide what theorem was used
to make the goal progress.

Signed-off-by: Ryan Lahfa <[email protected]>
@RaitoBezarius
Copy link
Contributor Author

@sonmarcho feel free to merge :)

@sonmarcho sonmarcho enabled auto-merge (squash) July 5, 2024 12:48
@sonmarcho sonmarcho merged commit 71f2c2a into AeneasVerif:main Jul 5, 2024
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants