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

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))