search

Deducteam / lambdapi

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

rewrite under quantifiers #1120

Closed bodeveix closed 1 week ago

bodeveix commented 1 week ago

The rewrite tactic fails to cross quantifiers as shown in the proof of the "bug" theorem of the attached file.

bug3.txt

fblanqui commented 1 week ago

Thank you for the issue. This is a known issue indeed. I close it since it is a duplicate of #694 .