Hi, all:<br><br>&nbsp;&nbsp; some issues around the redex<br><br>the code snippet:<br><br>(module test mzscheme<br>&nbsp; (require (planet &quot;reduction-semantics.ss&quot; (&quot;robby&quot; &quot;redex.plt&quot; 3)))<br>&nbsp; (define basic-grammar
<br>&nbsp;&nbsp;&nbsp; (language<br>&nbsp;&nbsp;&nbsp;&nbsp; (e x (e e) (&quot;lam&quot; x e))<br>&nbsp;&nbsp;&nbsp;&nbsp; (x variable-not-otherwise-mentioned)<br>&nbsp;&nbsp;&nbsp;&nbsp; ))<br>&nbsp; <br>&nbsp; (define ext-grammar<br>&nbsp;&nbsp;&nbsp; (extend-language<br>&nbsp;&nbsp;&nbsp;&nbsp; basic-grammar<br>&nbsp;&nbsp;&nbsp;&nbsp; (C number string )<br>
&nbsp;&nbsp;&nbsp;&nbsp; (e .... C)<br>&nbsp;&nbsp;&nbsp;&nbsp; ))<br>&nbsp; <br>&nbsp; (define-metafunction sub<br>&nbsp;&nbsp;&nbsp; basic-grammar<br>&nbsp;&nbsp;&nbsp; [(((x_1) ... x_2 x_3 ...) (x_4 ... x_2 x_5 ...))<br>&nbsp;&nbsp;&nbsp;&nbsp; (sub (((x_1) ... x_3 ...) (x_4 ... x_2 x_5 ...)))]<br>&nbsp;&nbsp;&nbsp; [(((x_1) ... x_2 x_3 ...) (x_4 ... ))
<br>&nbsp;&nbsp;&nbsp;&nbsp; (sub (((x_1) ... (x_2) x_3 ...) (x_4 ...)))]<br>&nbsp;&nbsp;&nbsp; [(((x_1) ...) (x_4 ... ))<br>&nbsp;&nbsp;&nbsp;&nbsp; (x_1 ...)])<br>&nbsp; <br>&nbsp; (define-metafunction fv<br>&nbsp;&nbsp;&nbsp; basic-grammar<br>&nbsp;&nbsp;&nbsp; [x_1 (x_1)]<br>&nbsp;&nbsp;&nbsp; [(e_1 e_2) ,(append (term (fv e_1)) (term (fv e_2)))]
<br>&nbsp;&nbsp;&nbsp; [(&quot;lam&quot; x_1 e_1) (sub ((fv e_1) (x_1)))]<br>&nbsp;&nbsp;&nbsp; )<br>&nbsp; <br>&nbsp; ;;?<br>&nbsp; (define-metafunction/extension fv1<br>&nbsp;&nbsp;&nbsp; ext-grammar<br>&nbsp;&nbsp;&nbsp; fv<br>&nbsp;&nbsp;&nbsp; [C_1 ()]<br>&nbsp;&nbsp;&nbsp; )<br>&nbsp; <br>&nbsp; (define ext2-grammar<br>&nbsp;&nbsp;&nbsp; (extend-language 
<br>&nbsp;&nbsp;&nbsp;&nbsp; ext-grammar<br>&nbsp;&nbsp;&nbsp;&nbsp; (prim + - * /)<br>&nbsp;&nbsp;&nbsp;&nbsp; (C .... prim)<br>&nbsp;&nbsp;&nbsp;&nbsp; (e .... prim)<br>&nbsp;&nbsp;&nbsp;&nbsp; )<br>&nbsp;&nbsp;&nbsp; )<br>&nbsp; <br>&nbsp; #;(define test (term (fv1 (&quot;lam&quot; y (&quot;lam&quot; x (+ x y))))))<br>&nbsp; <br>&nbsp; #;(define test2 (test-match ext2-grammar e_1 &#39;(+ (&quot;lam&quot; x (+ 1)))))
<br>&nbsp; <br>&nbsp; )<br><br>1. how can I use &quot;define-metafunction/extension&quot;?&nbsp; <br><br>firstly, it is inconvenient to rename fv to fv1<br>second, how can I reuse the definitions in fv?<br><br>btw, is there also a demo show on &quot;define-multi-arg-metafunction&quot;?
<br><br>2. a little suggestion: we see that ext2-grammar is something wrong which makes e and C all terminate on <br>prim. however, redex just accept it. so , test2 make multiple matches. For someone experienced to redex, 
<br>there is a quickly respond to the grammar. But, for the freshes, it takes time to handle. So, I suggest redex<br>do a static check on this case and report a warning<br><br>thanks<br><br>Gang<br>