The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello.

Can I make Coq to unify forall (x : X) {struct x}, A with T A, where T a := X -> A?
I need this type synonym for usage of some of my type classes, so I can't unwrap T A;
but I need to specify decreasing argument for my fixpoint definition.

Can I resolve that?

Sincerely,
Kirill Taran