Stream: general

Topic: Abstract over select occurrences of a term

Jannis Limperg (Jul 03 2020 at 17:24):

I'd like to have a tactic that takes an expression e and replaces some term s with t in e (like kabstract etc.) -- but only at certain locations within e. (Or, alternatively, everywhere in e except for certain 'blocked' locations.) Is this already a thing?

Example: Given the term x + x, I want to be able to say, "replace the first x but not the second."

Gabriel Ebner (Jul 03 2020 at 17:29):

I often use conv in ... { rw ... } for this.

Mario Carneiro (Jul 03 2020 at 17:31):

I think you can also use rw [] {occurrences := ...} for this

Jannis Limperg (Jul 03 2020 at 17:36):

Thanks! I'm not sure whether I'll be able to make rewrite-based tactics work for my particular problem, but I'll try.

Alex J. Best (Jul 03 2020 at 19:02):

You can make a lot of tactics into conv tactics, like ring and simp, this might fit your paradigm?

Last updated: May 08 2021 at 03:17 UTC