[racket] (where-not ...) in Redex

On Wed, Aug 29, 2012 at 3:28 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> On Aug 26, 2012, at 2:33 PM, Robby Findler wrote:
>
>
>
> On Sunday, August 26, 2012, Matthias Felleisen wrote:
>>
>>
>> On Aug 25, 2012, at 10:53 PM, Robby Findler wrote:
>>
>> > On Thu, Aug 23, 2012 at 8:11 AM, Matthias Felleisen
>> > <matthias at ccs.neu.edu> wrote:
>> >>
>> >> I would almost prefer the use of 'when' for 'where' and the
>> >> introduction of 'unless'.
>> >
>> > If we did this, then there could be no judgment-forms name 'when' or
>> > 'unless', which makes me think we shouldn't do this.
>>
>> I don't understand this point at all.
>>
>
> See the docs for define-judgement-form and imagine a judgment-form whose
> name was "unless". You'll notice a conflict in the premise grammar.
>
>
>
> I have taken the time to re-read the docs, and you're saying that someone
> could name a judgment rule 'when' or 'unless' via
> non-ellipsis-non-hyphen-var. Well, let them use strings if they must use
> such special names as rule names. For an SOS, I could imagine when_true and
> when_false as names, and for typing rules I could imagine when_t.

Sorry, no. I am saying that someone could write an actual
judgment-form named 'when' or 'unless'. And then they wouldn't be able
to use it in a premise.

Just like currently if someone defines a judgment-form named 'where'
they cannot use it in a premise.

(I will look into the other part of your message later.)

Robby