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

Add `unfold named_clause with ...` form #135

Open chaudhuri opened 3 years ago

chaudhuri commented 3 years ago

Todd Wilson (@lambdacalculator) suggests in the Abella mailing list that we should add a unfold named_clause with ... form to handle cases such as:

%:tapp:
of (tapp P E) (T P) :- typ P, of E (all T).

Here an invocation such as unfold tapp with T = ... might allow the clause to be potentially unfolded because it is no longer non-pattern after the substitution.