Clever Geek Handbook

Ltac: optional arguments

I want to do an Ltac tactic in coq that will take 1 or 3 arguments. I read about ltac_No_arg

in the module LibTactics

, but if I understood it correctly, I would have to use my tactic:

Coq < mytactic arg_1 ltac_no_arg ltac_no_arg.

which is not very convenient.

Is there a way to get this kind of result?

Coq < mytactic arg_1.

Coq < mytactic arg_1 arg_2 arg_3.
+3


source to share


1 answer


We can use a mechanism Tactic Notation

to try and solve your problem as it can handle variable arguments.

Reuse ltac_No_arg

and define mock tactics mytactic

for demonstration

Inductive ltac_No_arg : Set :=
  | ltac_no_arg : ltac_No_arg.

Ltac mytactic x y z :=
  match type of y with
  | ltac_No_arg => idtac "x =" x  (* a bunch of cases omitted *)
  | _ => idtac "x =" x "; y =" y "; z =" z
  end.

Now let's define the above tactical notation:



Tactic Notation "mytactic_notation" constr(x) :=
  mytactic x ltac_no_arg ltac_no_arg.
Tactic Notation "mytactic_notation" constr(x) constr(y) constr(z) :=
  mytactic x y z.

Tests:

Goal True.
  mytactic_notation 1.
  mytactic_notation 1 2 3.
Abort.
+4


source






More articles:


All Articles