I think in my case I actually do want the same nonterminal names. The
higher-order language has lambdas while the first-order language
doesn't. The first-order language has an outer `let' while the
higher-order language has no `let'. Every other kind of expression is
the same and has the same r
Yes, you guys are right-- this is not supported. You'd have to put
everything into a single language to make it work.
I've shied away from this because it seems overly complicated, but
also because the language names ("L1" and "L2" in Stephen's example)
don't show up anywhere in the typeset versio
On 02/05/2012 03:11 PM, Stephen Chang wrote:
I want to write a redex metafunction contract that goes between two
languages. Is there currently a way to do this?
For example,
#lang racket
(require redex)
(define-language L1
(e 1))
(define-language L2
(f 2))
(define-metafunction L1
L1->
I want to write a redex metafunction contract that goes between two
languages. Is there currently a way to do this?
For example,
#lang racket
(require redex)
(define-language L1
(e 1))
(define-language L2
(f 2))
(define-metafunction L1
L1->L2 : e -> f
[(L1->L2 1) 2])
> (term (L1->L2 1))
4 matches
Mail list logo
