Beluga icon indicating copy to clipboard operation
Beluga copied to clipboard

beli query's arguments inverted

Open Niols opened this issue 10 years ago • 0 comments

It looks like beli query's argument are not EXPECTED TRIES TYPE but TRIES EXPECTED TYPE.

For instance, after having defined:

nat : type.
z : nat.
s : nat -> nat.

I'm trying:

# %:query * 5 N : nat.
%query * 5

nat.

---------- Solution 1 ----------
[]
Empty substitution.
N = z.

...

---------- Solution 5 ----------
[]
Empty substitution.
N = s (s (s (s z))).

Done.
;

but:

# %:query * 5 N : nat.
%query * 5

nat.

---------- Solution 1 ----------
[]
Empty substitution.
N = z.

...

---------- Solution 322 ----------
[]
Empty substitution.
N = s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).

---------- Solution 323 ----------
[]
Empty substitution.
^C
;

I noticed it was the same for %query in files. I don't know where this is inverted, but it seems to be far in the code, since in Logic's more superficial functions this seems still to be the case…

Niols avatar Jul 27 '15 21:07 Niols