PasteRack.org
Paste # 70520
2024-03-20 09:54:32

Fork as a new paste.

Paste viewed 352 times.


Embed:

  1. #lang racket/base
  2. (require redex)
  3.  
  4. (define-language Lambda-Let
  5.   (e ::=
  6.      natural                    ; natural numbers
  7.      x                          ; variables
  8.      (lambda (x ...) e)         ; abstractions
  9.      (let ([x e] ...) e)        ; `let` forms
  10.      (e e ...))                 ; applications
  11.   (x ::= variable-not-otherwise-mentioned))
  12.  
  13. (define-metafunction Lambda-Let
  14.   let->lambda : e -> e
  15.   [(let->lambda (lambda (x ...) e_body))
  16.    (lambda (x ...) (let->lambda e_body))]
  17.   [(let->lambda (let ([x e] ...) e_body))
  18.    (let->lambda ((lambda (x ...) e_body) e ...))]
  19.   [(let->lambda (e ...))
  20.    ((let->lambda e) ...)]
  21.   [(let->lambda e)
  22.    e])
  23.  
  24. (term (let->lambda (let ([x 1]
  25.                          [y 2])
  26.                      (+ x y))))

=>