Pierre Vial (Dec 07 2020 at 14:45): Pierre Vial (Dec 07 2020 at 14:45):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)?
Gaëtan Gilbert (Dec 07 2020 at 14:48):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: Oct 13 2024 at 01:02 UTC