[Tactic] Rewrite Equiv

Overview

The main idea is to provide a way to rewrite a procedure call, somewhere in a program, into a different procedure call, using an equiv.

There is a variant provided to handle cases where the function to be rewritten to has different arguments and/or left-value than the instance provided.

Syntax

Same arguments: rewrite equiv[{m} p d lem]

Different arguments: rewrite equiv[{m} p d lem (a1, a2, ... :@ lv?)]

where

• m: 1 or 2
• p: code position
• d: direction, either - or nothing
• lem: equiv for the rewrite
• ai: an expression representing a function argument
• lv: a left-value

Permitted contexts

pRHL judgements

Examples

For examples tests/rwequiv.ec or instances in the standard library.