[racket-dev] Am I misusing judgment-holds ?

This is kind of awkward, tho. Do you plan to typeset this portion of your model?

Robby

On Wed, Aug 22, 2012 at 10:07 AM, Stephen Chang <stchang at ccs.neu.edu> wrote:
> Oh yeah, this first solution should work (I want to keep it as an
> output though). Thanks.
>
>
> On Wed, Aug 22, 2012 at 9:01 AM, Robby Findler
> <robby at eecs.northwestern.edu> wrote:
>> You could do the below, but can you say a little bit more about what
>> the metafunction and judgment-form you want to combine are?
>> (Presumably they both are type checking?)
>>
>> #lang racket
>> (require redex)
>>
>> (define-language L
>>   (e integer true false)
>>   (τ bool int))
>>
>> (define-judgment-form L
>>   #:mode (⊢ I O)
>>   #:contract (⊢ e τ)
>>   [(⊢ integer int)]
>>   [(⊢ true bool)]
>>   [(⊢ false bool)])
>>
>> (define-metafunction L
>>   [(type-checks? e τ)
>>    ,(member (term τ) (judgment-holds (⊢ e τ) τ))
>>    (side-condition (printf "τ = ~a\n" (term τ)))])
>>
>> (term (type-checks? true int))
>> (term (type-checks? true bool))