Skip to content

Rules with existential variables must retain \exists and restore variable names #3790

Open
@jberthold

Description

@jberthold

Existentials at the top of the RHS of rewrite rules are separated and the variables renamed (to avoid name clashes).
When such a rule is applied, the variables need to be renamed back in the result term, and the \exists re-added.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions