Patrick Nicodemus (Sep 10 2022 at 03:14): Patrick Nicodemus (Sep 10 2022 at 03:14):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?
Patrick Nicodemus (Sep 10 2022 at 03:17):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