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

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Wed Aug 22 09:20:33 EDT 2012

Oh, this variation may also be a better fit for what you want,
depending (note changed mode).


#lang racket
(require redex)

(define-language L
  (e integer true false)
  (τ bool int))

(define-judgment-form L
  #:mode (⊢ I I)
  #:contract (⊢ e τ)
  [(⊢ integer int)]
  [(⊢ true bool)]
  [(⊢ false bool)])

(define-metafunction L
  [(type-checks? e τ)
   ,(judgment-holds (⊢ e τ))])

(term (type-checks? true int))
(term (type-checks? true bool))

Posted on the dev mailing list.