I am working with Ltac2 on creating several tactics, and some of them require having an optional argument/variable.
I am wondering how to check whether the optional argument was indeed introduced when calling the tactic.
To put everything in context: I want to write a tactic that does the following: takes as “input” an
s(intropatterns) and an optional
constr input (as
t(opt(constr))). Is this the way of “enforcing” an optional variable?
If the above is the case, how can we, in this tactic, check whether or not the optional
constr is indeed “present” or not?
Would it work trying to match
empty? But, in this case, what would we match
t with if it is not empty?