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

Regression: Normalize should rename nested binders (2) #59

Closed robblanco closed 8 years ago

robblanco commented 8 years ago

From test/test_metaterm.ml:

Failure: Abella:4:Metaterm:33:Normalize should rename nested binders (2)

OUnit: expected: forall A2, A = A1 -> (forall A1, A1 = A1) but got: forall A2, A = A1 -> (forall A3, A3 = A3)
chaudhuri commented 8 years ago

This does not seem to be a bug. Normalization was rewritten sometime after 2.0.x and does alpha-variance differently. The test needs to be updated.