\Citet{mcdonell_embedded_2022} extends on this idea, resulting in a very similar but different solution to ours.
They used the technique that \citeauthor{atkey_unembedding_2009} showed and applied it to deep embedding using the concrete syntax of the host language.
The scaffolding---e.g.\ generating the pairs, sums and injections---for embedding is automated using generics but the required pattern synonyms are generated using \gls{TH}.
\Citet{mcdonell_embedded_2022} extends on this idea, resulting in a very similar but different solution to ours.
They used the technique that \citeauthor{atkey_unembedding_2009} showed and applied it to deep embedding using the concrete syntax of the host language.
The scaffolding---e.g.\ generating the pairs, sums and injections---for embedding is automated using generics but the required pattern synonyms are generated using \gls{TH}.