Hello,

I would like to define a simple Ltac tactic on pair of lists.

Let's say for instance that I want a dummy tactic that computes the sum of the length of two listes. I would write something like:

```
Ltac sum_length_tac l1 l2 :=
match (l1 , l2) with
| (nil , nil) => O
| (_ :: ?s1 , _ ?s2) => constr:(S (S (sum_length_tac s1 s2)))
| _ => constr:(S O)
end.
```

I get the nice error message:

```
Error:
Syntax error: ')' expected after [tactic:tactic_expr] (in [tactic:tactic_expr]).
```

But is it just possible to match on pair? Is there some `constr:`

missing somewhere e.g. before `(l1,l2)`

?

```
Ltac sum_length_tac l1 l2 :=
match constr:((l1 , l2)) with
| (nil , nil) => O
| (cons _ ?s1 , _ ?s2) =>
let s := sum_length_tac s1 s2 in
constr:(S (S s))
| _ => constr:(S O)
end.
Goal False.
let x := sum_length_tac (cons 0 (cons 1 nil)) (cons 0 (cons 1 nil)) in
idtac x.
```

Thanks Gaëtan!

Last updated: Feb 08 2023 at 23:03 UTC