We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
take
drop
Here's what happens if you try:
sawscript> prove do { goal_eval_unint ["take"];} {{ \ (x : [8]) -> take`{2} (x ^ x) == take`{2} x ^ take`{2} x }} Stack trace: "prove" (<stdin>:1:1-1:6): "goal_eval_unint" (<stdin>:1:12-1:27): could not create uninterpreted function argument of type PrimName {primVarIndex = 135, primName = Prelude.Nat, primType = sort 0}
The text was updated successfully, but these errors were encountered:
Also, that PrimName {primVarIndex... nonsense in the error message needs to be fixed.
PrimName {primVarIndex...
Sorry, something went wrong.
Make goal_eval_unint handle functions with arguments of type Nat.
goal_eval_unint
Nat
0d99509
We can now make functions like `take` and `drop` uninterpreted. Fixes #1588.
147209b
Successfully merging a pull request may close this issue.
Here's what happens if you try:
The text was updated successfully, but these errors were encountered: