[plt-scheme] redex: discarding a sub-syntactic form

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Sat Sep 12 19:56:46 EDT 2009

How about defining another syntactic category that only includes l and
f and then use that to reduce?

But if you wanted a side-condition, you could write it with
redex-match, ie (not (redex-match <lang> (with igv igv) (term


On Sat, Sep 12, 2009 at 3:38 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> Hi,
> I have another question with redex:
> I have a syntactic category:
> (igv l f (with igv igv))
> I want to define a reduction rule for the "atomic" cases where igv is either
> l or f,
> and another one for the "compounded" case (with igv igv).
> If I do so and don't put a side condition, then of course the reduction
> relation becomes non-determinist.
> So I'm trying to add a side condition for the atomic case that discards the
> compounded case. Something like:
>   (side-condition (not (eq? (term igv) (term (with igv_1 igv_2)))))
> this however does not seem to do the job. I tried with (not (match... )) but
> then I get an error related to with ("with: used outside of
> reduction-relation").
> I really want to say "where igv is not of the form (with x y)".
> Any clue/suggestion?
> Thanks in advance,
> -- Éric
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme

Posted on the users mailing list.