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

 From: Matthias Felleisen (matthias at ccs.neu.edu) Date: Wed Aug 29 16:28:48 EDT 2012 Previous message: [racket] (where-not ...) in Redex Next message: [racket] (where-not ...) in Redex Messages sorted by: [date] [thread] [subject] [author]

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.

>  >> The type setting of 'when' could still use 'where' as the English word (and perhaps we can have a way to override it).
> >>
> >> I am not sure how to type set 'unless' other than by providing a the negative operator as an argument !=
> >
> > Using \neq{} seems right to me.
>
> What if you want \not\in or \not\subtype and such?
>
>
> You can't use where or unless for such things already. Either that or I don't understand you?
>

How would you formulate judgments like this:

|- e -> v
------------------------ when v in Nat & v > 0
|- (foo e bar e_1) -> v[e_1}

-- Matthias

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120829/7f4c9012/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4373 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20120829/7f4c9012/attachment-0001.p7s>


 Posted on the users mailing list. Previous message: [racket] (where-not ...) in Redex Next message: [racket] (where-not ...) in Redex Messages sorted by: [date] [thread] [subject] [author]