Ssreflect Users Discussion List

[ben <>]

Hello,

i am formalizing category theory in Coq, and i was wondering whether
reflection could help with the automation of some proofs.

From Yves' book i know how reflection works in theory. Nevertheless it
would be nice to see some real life example of a proof in some algebraic
theory done by reflection, in order to get a better feeling for what
kind of problems are suitable for being treated with this technique.

Could you point me to an example, a theorem (of, say group theory ?)
where reflection was particularly helpful ?

Thanks a lot in advance,
ben