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: Oct 13 2024 at 01:02 UTC