search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Query broken in 2.0.4 due to missing argument to Tactics.search #69

Closed chaudhuri closed 7 years ago

chaudhuri commented 7 years ago

This bug report was posted to the mailing list by @kyagrd. 

kyagrd@kyagrd:~/tmp$ uname -a
Linux kyagrd 4.8.0-1-amd64 #1 SMP Debian 4.8.5-1 (2016-10-28) x86_64 GNU/Linux
kyagrd@kyagrd:~/tmp$ cat a.thm
Kind t type.
Type v t.

Define p : t -> prop by p v.
kyagrd@kyagrd:~/tmp$ abella -v
2.0.4
kyagrd@kyagrd:~/tmp$ abella -i a.thm
Welcome to Abella 2.0.4
Abella < Kind t type.

Abella < Type v t.

Abella < Define p : t -> prop by
p v.

Abella < Switching to interactive mode.
Abella < Query p X. % expecting X = v but ...
No more solutions.

Abella < Query true.
No more solutions.

Abella < Query false.
No more solutions.