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 (⊢
Oh, this variation may also be a better fit for what you want,
depending (note changed mode).
Robby
#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)]
[(⊢
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
ro...@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
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 stch...@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
I'm using it as a side condition so if I need to typeset, I can just
add a wrapper macro to make it look nicer?
Something like:
#lang racket
(require redex)
(define-language L
(e integer true false)
(τ bool int))
(define-judgment-form L
#:mode (⊢_ I O)
#:contract (⊢_ e τ)
[(⊢_
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
6 matches
Mail list logo
