Ssreflect Users Discussion List

[Florent Hivert <>]

      Hi there,

Is there a way to use bigop with function composition ?

Suppose that I have an eqType (unfortunately not finite) T. The functional
composition \o together with identity id defines mathematically a monoid but
unless I suppose functional extensionality on T, I can only use =1 and not =
to compare two functions. As a consequence, I can't manage to define a proper
Monoid.law for \o and id. Is there a simple solution ?

Cheers,

Florent Hivert