I have a pattern and I want to write a tactic that takes in a term and succeeds if the pattern matches on some subterm and fails otherwise. Other than that, I don't want it to do anything.
Can I do this in SSReflect?
Another, related question. The 'in' tactical in SSReflect doesn't let me write
set x := t in *.
Is there a way I can replace all terms t with x?
Last updated: Dec 07 2023 at 17:01 UTC