Можно ли реализовать в PLT-Redex выражение, подобное let *?

Question

Недавно я начал использовать PLT-Redex, и мне интересно, может ли кто-нибудь дать мне несколько указаний о том, как реализовать выражение let *, как в Racket.

Прямо сейчас я могу писать простые выражения let вроде этого

(let (x (+ 2 4)) in (* x 2))
(let (x (+ 2 4)) in (let (y (* x 2)) in y))

Однако, если я попробую сложные выражения let, подобные приведенным ниже (см. Тест 4 и 5 в моем коде), я получу несколько выходных значений:

(let (x (+ 2 4)) in (let (y (* x 2)) in (* y y)))
(let (x (+ 2 4)) in (let (y (* x 2)) in (let (y (* x 2)) in (let (z (+ y 5)) in (+ (+ x y) z)))))

Я хотел бы переписать приведенное выше выражение так

(let* ([x (+ 2 4)]
       [y (* x 2)]
       [z (+ y 5)]
    (+ (+ x y) z))

Ниже представлена ​​моя текущая реализация Redex на случай, если кто-то захочет помочь.

Заранее спасибо Умберто

#lang racket
(require redex)

(define-language L
  (e ::=
     v
     x
     (let (x e) in e)
     (e ...)
     (aop e e))

  (v ::= number integer string boolean)
  (x  ::= variable-not-otherwise-mentioned)
  (aop ::= + - / *)

  (p (e ...))
  (P (e ... E e ...))
  
  (E ::= 
     hole
     (let (x E) in e)
     (aop E e))

);; 


(define-metafunction L
  [(subst (x_1 any_1 x_1)) any_1]
  [(subst (x_1 any_1 x_a)) x_a]

  [(subst (x any (let (x e_x) in e_body)))
   (let (x (subst (x any e_x))) in e_body)]

  [(subst (x any (let (x_a e_xa) in e_body)))
   (let (x_a  (subst (x any e_xa))) in (subst (x any e_body)))]

  [(subst (x any (aop e_1 e_2)))
   (aop (subst (x any e_1)) (subst (x any e_2)))]

  [(subst (x any v_2)) v_2]
);;

(define L-R
  (reduction-relation
   L            
   #:domain p
 
   (--> 
    (in-hole P (/ number_1 0))
    ,(error 'DivisionByZeroError)
    "error")
   
   (--> 
    (in-hole P (+ number_1 number_2))
    (in-hole P ,(+ (term number_1) (term number_2)))
    "add")
   
   (-->
    (in-hole P (* number_1 number_2))
    (in-hole P ,(* (term number_1) (term number_2)))
    "multiply")
   
   (-->
    (in-hole P (/ number_1 number_2))
    (in-hole P ,(/ (term number_1) (term number_2)))
    "divide")
   
   (--> 
    (in-hole P (- number_1 number_2))
    (in-hole P ,(- (term number_1) (term number_2)))
    "subtract")

    (-->
     (in-hole P (let (x_1 e_1) in e_2))
     (in-hole P (subst (x_1 e_1 e_2))) 
    "let")
));;;

(define (test-syntax)
  ;; Test 1
  (test-->> L-R
            (term  ((+ 2 3)))
            (term  (5)))
  
 ;; Test 2
  (test-->> L-R
            (term  ((let (x (+ 2 4)) in (* x 2))))
            (term  (12)))
  
  ;; Test 3
  (test-->> L-R
            (term  ((let (x (+ 2 4)) in (let (y (* x 2)) in y))))
            (term  (12)))
  
  ;; Test 4 ERROR
;  (test-->> L-R
;            (term  ((let (x (+ 2 4)) in (let (y (* x 2)) in (* y y)))))
;            (term  (144)))


  ;; Test 5 ERROR
;  (test-->> L-R
;            (term  ((let (x (+ 2 4)) in (let (y (* x 2)) in (let (y (* x 2)) in (let (z (+ y 5)) in (+ (+ x y) z)))))))
;            (term  (35)))


);;


(test-syntax)
(module+ test
  (test-results))