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)) . . ..\..\plt\collects\redex\private\error.rkt:3:0: L1->L2: codomain test failed for 2, call was (L1->L2 1) Switching the metafunction language to L2 similarly produces an error about the domain. Currently it seems like I can't use a contract with these kinds of metafunctions. How difficult would it be to support this functionality? It seems like this use case should be pretty common. I'm imagining something like: (define-metafunction L1->L2 : L1:e -> L2:f [(L1->L2 1) 2]) _________________________ Racket Developers list: http://lists.racket-lang.org/dev
