Stream: math-comp users

Topic: Questions on matching


view this post on Zulip 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?

view this post on Zulip 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: Jan 29 2023 at 19:02 UTC