Hi, I am fairly new to elpi, I hope this in the right place to ask newbie questions.
What's the meaning of the error message "Evaluation of a non closed term (maybe delay)"?
Hello, the place is absolutely right.
This program raises that error
main :- X is A + 1.
A has no value
The maybe delay part is because
X is A + 1, A = 0 could still work if one suspends the first part until the second executes
Ok.. I don't think I see what I am doing wrong.
So I defined a predicate
pred p i:int. p K :- K > 0.
and I would like elpi to find me such a K when I do
p K, coq.say K
> is a builtin which does not "generate", it only tests.
Also note that you defined
p taking the argument in
input (it plays no role here, but is fishy).
What are you trying to do actually, the big picture.
I was trying to figure out how to write a sudoku solver.
so, elpi is not a constraint solver. your integers are a finite domain, so I see why it made sense.
you can still write something like
p 1. p 2. p 3. ... etc ....
and there elpi will try with any of these, when you ask
Last updated: Feb 05 2023 at 14:02 UTC