Stream: Coq users

Topic: ✔ Problem with recursive pattern in notations


view this post on Zulip 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 !

view this post on Zulip Notification Bot (Mar 03 2023 at 18:29):

Pierre Castéran has marked this topic as resolved.


Last updated: Jun 16 2024 at 02:41 UTC