Notation for list with fixed type
I am using the following notations in RefinedC:
Notation "'[@{' A '}' x ; y ; .. ; z ]" := (@cons A x (@cons A y .. (@cons A z (@nil A)) ..)) (only parsing) : list_scope.
Notation "'[@{' A '}' x ]" := (@cons A x nil) (only parsing) : list_scope.
Notation "'[@{' A '}' ]" := (@nil A) (only parsing) : list_scope.
Would it be useful to upstream them to stdpp?