Rocq: Transparent aliased definition (that instance solver sees though)

Question

In Rocq, we can define aliases for types or other elements using Definition.

Unfortunately, these aliases often break typeclass resolution and require explicit unfolding within proofs.

In some cases, Notation is an option, but this cannot give non-symbolic names.

Is there a way to give something another name such that it expands trivially within proofs and instance resolution?

Answer 1

There is a restricted form of notations, called abbreviations, which don't create new tokens, but are instead parsed as regular names.

Notation new_constant := a_term.
Notation f x y z := (g z x y).