<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Aug 26, 2012, at 2:33 PM, Robby Findler wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><br><br>On Sunday, August 26, 2012, Matthias Felleisen wrote:<br><blockquote class="gmail_quote" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; position: static; z-index: auto; "><br>
On Aug 25, 2012, at 10:53 PM, Robby Findler wrote:<br>
<br>
> On Thu, Aug 23, 2012 at 8:11 AM, Matthias Felleisen<br>
> <<a href="javascript:;" onclick="_e(event, 'cvml', 'matthias@ccs.neu.edu')">matthias@ccs.neu.edu</a>> wrote:<br>
>><br>
>> I would almost prefer the use of 'when' for 'where' and the introduction of 'unless'.<br>
><br>
> If we did this, then there could be no judgment-forms name 'when' or<br>
> 'unless', which makes me think we shouldn't do this.<br>
<br>
I don't understand this point at all.<br>
<br></blockquote><div><br></div><div>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. </div></blockquote><div><br></div><div><br></div><div>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. </div><div><br></div><div><br></div><br><blockquote type="cite"><div> >> The type setting of 'when' could still use 'where' as the English word (and perhaps we can have a way to override it).</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
>><br>
>> I am not sure how to type set 'unless' other than by providing a the negative operator as an argument !=<br>
><br>
> Using \neq{} seems right to me.<br>
<br>
What if you want \not\in or \not\subtype and such?<br>
<br></blockquote><div><br></div><div>You can't use where or unless for such things already. Either that or I don't understand you?<span></span></div><div><br></div></blockquote><br></div><div>How would you formulate judgments like this: </div><div><br></div><div> |- e -> v </div><div> ------------------------ when v in Nat & v > 0 </div><div> |- (foo e bar e_1) -> v[e_1}</div><div><br></div><div><br></div><div>-- Matthias</div><div><br></div></body></html>