Ssreflect Users Discussion List

[Benjamin Gregoire <>]

ben wrote:
> 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 ?
>
>   
  The tactics ring, field, romega can be examples.

> Thanks a lot in advance,
> ben
>
>