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

Q.PAT_ABBREV_TAC should do type instantiation #252

Closed
xrchz opened this Issue Apr 15, 2015 · 5 comments

Comments

Projects
None yet
2 participants
@xrchz
Copy link
Member

xrchz commented Apr 15, 2015

Q.PAT_ABBREV_TAC often fails when the given pattern fails to match only because of a too general type. I think functionality would be strictly better if, instead of failing, it tried a match that did not require matching types.

@mn200

This comment has been minimized.

Copy link
Member

mn200 commented May 26, 2015

I don't understand the issue. If you have a pattern with a general type, it does instantiate:

Q.MATCH_ABBREV_TAC `P x` ([], ``y * 6 < 10``);
val it =
   ([([``Abbrev (x = 10)``,
       ``Abbrev (P = $< (y * 6))``],
      ``P x``)], fn) : goal list * validation

And if the goal has a more general type than the pattern, I don't understand what you'd want to see.

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented May 26, 2015

I'm talking about PAT_ABBREV_TAC, not MATCH_ABBREV_TAC

@mn200

This comment has been minimized.

Copy link
Member

mn200 commented May 26, 2015

D'oh! I'm not even sure I know what PAT_ABBREV_TAC does.

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented May 26, 2015

Maybe you could reimplement Q.PAT_ABBREV_TAC in terms of Q.MATCH_GOALSUB_ABBREV_TAC (although I just noticed that that doesn't exist).

@mn200

This comment has been minimized.

Copy link
Member

mn200 commented May 26, 2015

It's an easy fix in fact. Commit coming.

@mn200 mn200 closed this in 70bcf8e May 26, 2015

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment