Am Mo., 26. Dez. 2022 um 12:52 Uhr schrieb Amirouche <xxxxxx@hyper.dev>:
>
> > > What should happen when the same ⟨pattern variable⟩ appears more than one time in a pattern?
> >
> >
> > For example
> >
> > (match '(42 42 nothing)
> > ((,a ,a . rest) a))
> >
> > In my opinion, the above expression should eval to 42.
> >
>
> It appears, I am mistaken:
>
> > In each ⟨pattern⟩, the ⟨pattern variables⟩ and ⟨cata variables⟩ must be pairwise disjoint (in the sense of bound-identifier=?).
>
> Can you confirm that my new understanding is correct: variables whether they are pattern variables, or cata variable should appears once in a pattern?

Yes; for your (42 42 nothing) example from above, use a guard clause:

(match '(42 42 nothing)
  ((,a1 ,a2 . rest) (guard (= a1 a2)) a1))

This also circumvents the problem of which equivalence predicate to choose.

PS A cata variable can coincide with a pattern variable, but not with
another cata variable.