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

2012-08-29 Thread Matthias Felleisen
No they are just special instances of 'side' but I think for all of these keywords would be better. On Aug 29, 2012, at 5:54 PM, Robby Findler wrote: > Where is a binding form. > > Did you mean #:when and #:unless to be binding forms or not? > > Robby > > On Wed, Aug 29, 2012 at 4:49 PM, M

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

2012-08-29 Thread Robby Findler
Where is a binding form. Did you mean #:when and #:unless to be binding forms or not? Robby On Wed, Aug 29, 2012 at 4:49 PM, Matthias Felleisen wrote: > > Good enough. I thought of using 'where' but 'side' is better. > > > On Aug 29, 2012, at 5:46 PM, Robby Findler wrote: > >> (define-judgment-

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

2012-08-29 Thread Matthias Felleisen
Good enough. I thought of using 'where' but 'side' is better. On Aug 29, 2012, at 5:46 PM, Robby Findler wrote: > (define-judgment-form L > #:mode (-> I O) > [(-> e v) > (side-condition (positive-nat v)) > --- > (foo e bar e_1) -> (v e_1)] > > (define-metafunct

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

2012-08-29 Thread Robby Findler
On Wed, Aug 29, 2012 at 3:28 PM, Matthias Felleisen 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 >>

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

2012-08-29 Thread Matthias Felleisen
p.s. and you really want to say 'when' and 'unless' in the rules I suggested, and they do need proper type setting. On Aug 29, 2012, at 5:33 PM, Robby Findler wrote: > On Wed, Aug 29, 2012 at 4:14 PM, Matthias Felleisen > wrote: >> >> On Aug 29, 2012, at 5:10 PM, Robby Findler wrote: >> >>

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

2012-08-29 Thread Matthias Felleisen
keywords sound wonderful. On Aug 29, 2012, at 5:33 PM, Robby Findler wrote: > On Wed, Aug 29, 2012 at 4:14 PM, Matthias Felleisen > wrote: >> >> On Aug 29, 2012, at 5:10 PM, Robby Findler wrote: >> >>> Sorry, no. I am saying that someone could write an actual >>> judgment-form named 'when' o

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

2012-08-29 Thread Robby Findler
On Wed, Aug 29, 2012 at 4:14 PM, Matthias Felleisen wrote: > > On Aug 29, 2012, at 5:10 PM, Robby Findler wrote: > >> 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 curre

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

2012-08-29 Thread Matthias Felleisen
On Aug 29, 2012, at 5:10 PM, Robby Findler wrote: > 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

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

2012-08-29 Thread Robby Findler
On Wed, Aug 29, 2012 at 3:28 PM, Matthias Felleisen 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 >>

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

2012-08-29 Thread Matthias Felleisen
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 > > wrote: > >> > >> I would almost prefer the use of 'when' for 'whe

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

2012-08-26 Thread Robby Findler
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 > > > wrote: > >> > >> I would almost prefer the use of 'when' for 'where' and the > introduction of 'unless'. > > > > If we did th

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

2012-08-26 Thread Matthias Felleisen
On Aug 25, 2012, at 10:53 PM, Robby Findler wrote: > On Thu, Aug 23, 2012 at 8:11 AM, Matthias Felleisen > 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',

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

2012-08-25 Thread Robby Findler
On Thu, Aug 23, 2012 at 8:11 AM, Matthias Felleisen 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. > The type setting of

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

2012-08-23 Thread Matthias Felleisen
I would almost prefer the use of 'when' for 'where' and the introduction of 'unless'. 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

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

2012-08-22 Thread Asumu Takikawa
Hi all, Had a question/feature request for Redex. In various models, I've encountered situations where I wanted the dual behavior to the (where pattern term) clause of Redex (i.e., does term *not* match this pattern). In the past, I've used side-conditions or where clauses with predicate metafunc