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
The query length l == 10 does not work via SMT due to lack of fuel. So we can attempt to use meta-args to solve the squash via normalization, which should work fine, but does not.
I would have expected the implicit to be solved by the tactic, and not need any re-checking, but apparently some re-checking is done and so this fails. At least, the rechecking should be done on the rewritten type..?
The query
length l == 10
does not work via SMT due to lack of fuel. So we can attempt to use meta-args to solve the squash via normalization, which should work fine, but does not.I would have expected the implicit to be solved by the tactic, and not need any re-checking, but apparently some re-checking is done and so this fails. At least, the rechecking should be done on the rewritten type..?
This seems to be previous to all the #3134 stuff.
The text was updated successfully, but these errors were encountered: