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

Remove stripping of conjunctions from `irule` #465

Closed
xrchz opened this issue Sep 28, 2017 · 2 comments

Comments

Projects
None yet
2 participants
@xrchz
Copy link
Member

commented Sep 28, 2017

Extracts from messages on the HOL info mailing list:

I find it annoying that irule produces lots of new subgoals for the hypotheses. Is there a version that doesn't strip all the conjunctions, so they can be worked on together?

I agree about the stripping of conjunctions. My temptation is to just remove that feature entirely; making the user follow up with rpt conj_tac if that’s what they want doesn’t seem much of an imposition.

@mn200

This comment has been minimized.

Copy link
Member

commented Oct 24, 2017

I'm totally sympathetic to this, but we documented this behaviour in the Kananaskis-11 release. Perhaps we should avoid introducing a backwards incompatibility. We could come up with another name for the behaviour without the strip_conj. What about rule, say?

@xrchz

This comment has been minimized.

Copy link
Member Author

commented Oct 24, 2017

No, I think the behaviour and documentation should be updated.

Additional thought: could we change match_mp_tac to be irule without conjunction stripping? Is that a superset of its current behaviour? (and does the backwards incompatibility of reducing failures matter?)

@mn200 mn200 added this to the Kananaskis-12 milestone May 15, 2018

@mn200 mn200 closed this in d2d6d79 May 21, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.