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.

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

Jump to bottom

Proof tactics for applying introduction rules #92

Closed
brianhuffman opened this issue Jan 13, 2016 · 1 comment
Closed

Proof tactics for applying introduction rules #92

brianhuffman opened this issue Jan 13, 2016 · 1 comment
Labels
type: enhancement Issues describing an improvement to an existing feature or capability

Comments

@brianhuffman
Copy link
Contributor

We need to have a proof tactic for applying a Theorem as an introduction rule to the current proof goal. Also it would be useful to have a tactic for repeatedly applying rules from a given set as long as they match.

Note that this feature would only really make sense once we've implemented proof states with multiple goals (part of issue #9).
@brianhuffman brianhuffman added the type: enhancement Issues describing an improvement to an existing feature or capability label Jan 13, 2016
@brianhuffman
Copy link
Contributor Author

This is already implemented with the goal_apply command.

brianhuffman pushed a commit that referenced this issue Apr 26, 2021
Merge pull request #92 from GaloisInc/unint-poly
066e7a8 
Support uninterpreted polymorphic functions in sbv/what4 backends.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@brianhuffman