[plt-scheme] redex: leveraging generated checks and coverage

On Sep 17, 2009, at 7:23 PM, Casey Klein wrote:
>
> `name' is just a way to bind a name to a piece of a term so that you
> can refer to it in your test expression.
> [...]
> `name' can also be used in defining metafunctions and reduction
> relationsto give a name to a piece of the left-hand side for use in
> the right-hand side.

Sweet, I had completely missed that :/

> The space is probably going to the caches Redex uses to speed up
> matching and metafunction application. Addressing this problem is on
> my TODO list.

Ok, great.

> Your hand-crafted test suite must not have tried a case where the
> metafunction in question produced multiple results.

Indeed, since it produced multiple results only on bad terms (eg. a  
store with non-unique locations).

Thanks for all the clarifications!

-- Éric