Pierre Castéran (Mar 02 2023 at 15:34): Pierre Castéran (Mar 02 2023 at 15:34):I would like to define a notation for printing and parsing long sequences of substitutions. Unfortunately, my attempts to use recursive patterns resulted in error messages. Is there a simple solution?
Parameter term formula: Set.
Parameter subst : formula -> nat -> term -> formula.
Variable t1 t2 t3: term.
Variable f : formula.
Check subst (subst (subst f 1 t1) 2 t2) 3 t3.
(** should be parsed/printed as (substn f [(1, t1); (f2, t2); (3,t3)])
*)
Fail Notation "substn f [ ( v1 , t1 ) ; .. ; ( vn , tn ) ]" :=
(subst .. (subst f v1 t1) .. vn tn).
(*
The command has indeed failed with message:
The token ";" occurs on one side of ".." but not on the other side.
*)
Fail Notation "substn f [ ( v1 , t1 ) ; ( v2 , t2 ) ; .. ; ( vn , tn ) ]" :=
(subst .. (subst f (subst f v1 t1) v2 t2) .. vn tn).
(*
The command has indeed failed with message:
The token ";" occurs on one side of ".." but not on the other side.
*)
Ups, I didn't notice https://github.com/coq/coq/issues/7959 !
Notification Bot (Mar 03 2023 at 18:29):Pierre Castéran has marked this topic as resolved.
Last updated: Oct 08 2024 at 15:02 UTC