I want to use judgment-holds in a side-condition but sometimes it doesn't quite work because it's a macro. In the following example, judgment-holds does not use the value bound to tau. Is there a nice way to make it do what I want?
#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)] [(⊢ true bool)]) (define-metafunction L [(type-checks? e τ) ,(judgment-holds (⊢ e τ)) (side-condition (printf "τ = ~a\n" (term τ)))]) Welcome to DrRacket, version 5.3.0.20 [3m]. Language: racket [custom]. > (judgment-holds (⊢ 1 int)) #t > (judgment-holds (⊢ 1 bool)) #f > (term (type-checks? 1 int)) τ = int #t > (term (type-checks? 1 bool)) τ = bool #t _________________________ Racket Developers list: http://lists.racket-lang.org/dev