Consider a lemma such as sb_ret: one of the sides shouldn't need type annotation.
The problem amount to the following in a minimal setup:
Section foo.
Variable F : Type -> Type.
Variable EQ : forall X Y, F X -> F Y -> Prop.
Variable cst : forall X, F X.
Infix "≃" := (@EQ _ _) (at level 70).
Fail Goal cst _ ≃ cst unit. (* Indeed, nothing constraints the _, fair: can we do better? *)
Note that the following doesn't work, as the notation is just expanded into two holes before it is elaborated into an evar.
Notation EQ_hom X := (@EQ X X). (* Attempt at telling Rocq both sides have the same type *)
Infix "≅" := (EQ_hom _) (at level 70).
Goal cst _ ≅ cst unit. (* Still doesn't work *)
However the following suggested by Jan-Oliver Kaiser on Zulip works:
Notation EQ_hom X := (match X with _X => @EQ _X _X end).
Infix "≅" := (EQ_hom _) (at level 70).
Goal cst _ ≅ cst unit. (* Works! *)
TODO: experiment with this trick and see if it is robust enough to incorporate.
Consider a lemma such as sb_ret: one of the sides shouldn't need type annotation.
The problem amount to the following in a minimal setup:
Note that the following doesn't work, as the notation is just expanded into two holes before it is elaborated into an evar.
However the following suggested by Jan-Oliver Kaiser on Zulip works:
TODO: experiment with this trick and see if it is robust enough to incorporate.