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
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.
Last updated: Oct 04 2023 at 22:01 UTC