search

abella-prover / abella

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

Query and search seem to disagree #32

Closed chaudhuri closed 9 years ago

chaudhuri commented 10 years ago

This works:

Kind i type.
Type p i -> o.
Theorem foo : exists X, {p n1 |- p X}. search.

This doesn't work (produces no solutions).

Query {p n1 |- p X}.