search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
265 stars 35 forks source link

Rewriting a pattern containing an abstraction #862

Open QGarchery opened 2 years ago

QGarchery commented 2 years ago

Hi again !

Rewriting a pattern that contains an abstraction does not seem to work anymore. For example, running lambdapi version 2.2.0 on the content of rew_abs.txt fails with Uncaught [File "src/handle/rewrite.ml", line 172, characters 18-24: Assertion failed].

Note that this file was verified with lambdapi version 2.1.0, and that this issue is similar to #670 but concerns the pattern to rewrite instead of the term to be rewritten.

fblanqui commented 2 years ago

Change introduced in #834. Will try to fix it.