Ltac2: checking if an optional input variable is present

Developing plugins
1

Dear community,

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 t with empty? But, in this case, what would we match t with if it is not empty?

2

The opt scope returns an option, which is an algebraic datatype with two constructors None and Some. Pattern-matching on the value with those two cases is thus enough to perform what you describe.

3

This indeed worked. Thank you!