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

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>