[plt-scheme] [redex] what computation is happening?

Hi,

I'm wondering what happens exactly when one "runs" a redex module that has no tests/traces at all.

I have one language definition and one reduction relation (admittedly both quite complex, around 300 lines with generous indentation), and when I click "run" it takes around 40 seconds before I get the prompt back in the interaction window. 

So something substantial must be going on, I'd like to know what. 

In particular, that computation was able to find places where I forgot to use ellipsis for instance, but not able to report parts where I use undefined metafunctions (I use around 20 as-yet-undefined metafunctions in the reductions). I doubt that these 40 seconds are only used to check for proper uses of ellipses...

(I'm on 4.2.5, mac os 10.6)

Thanks!

-- Éric