Wrong scoping of rule LHS on AC symbols - Githubissues

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

Other

265 stars 35 forks source link

Wrong scoping of rule LHS on AC symbols #992

Open fblanqui opened 1 year ago

fblanqui commented 1 year ago

When scoping rule LHS of AC symbols, AC-canonization should be deactivated.