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 > > <matth...@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
smime.p7s
Description: S/MIME cryptographic signature
____________________ Racket Users list: http://lists.racket-lang.org/users
