Skip to content

qmatch_abbrev_tac should rename var/var bindings rather than abbreviate them #1085

New issue
New issue
Open
Open
qmatch_abbrev_tac should rename var/var bindings rather than abbreviate them#1085
Labels
Feature RequestTactics/DPs
@mn200

Description

@mn200
mn200
opened on Jan 5, 2023

Introducing an Abbrev(newv = oldv) assumption seems wasteful; should just rename (as per that tactic) the occurrences of oldv into newv.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Feature RequestTactics/DPs

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions