Is there a simple way to define a notation for sequences of substitutions?

Let us consider the following context:

```
Parameter Exp:Set.
Definition var := nat.
Parameter subst : Exp -> var -> Exp -> Exp.
```

I would like to build a notation `msubst e v1 <- t1 ; v2 <- t2; ... ; vn <- tn`

for `subst ... (subst e v1 t1) v2 t2) ... vn tn`

.

I would prefer not to define `msubst`

as a function, since it would break very long proof scripts which use nested `subst`

s.

Are custom entries the right tool for that?

Naively, it seems like this should be possible with recursive notations, no custom entries seem necessary? Or did you notice some problem I'm missing?

https://plv.mpi-sws.org/coqdoc/iris/iris.bi.lib.atomic.html uses recursive notations on a larger example — sorry I don't have code for your example, but Coq notations never seem to be 5-minute affairs.

Thanks @Paolo Giarrusso

There exists a thread on this topic already. I will have to check if there exists a solution which satisfies my constraints (some long scripts in the `goedel`

library contain nested substitutions, and I'm looking for readable notations for these big terms).

Ooh I see, that link points to custom entries indeed

Last updated: Jun 23 2024 at 05:02 UTC