(module closure-calculus mzscheme
(require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2 2)))
(provide (all-defined))
(define lang
(language
(e hole
(e c)
(v e))
(s (v ...))
(t number
(t t)
(lambda t))
(c (t s)
(c c))
(v ((lambda t) s))))
(define reductions
(list
(reduction/context/name
"Beta" lang e
(((lambda t_0) s_0) v_0)
(term (t_0 (v_0 . s_0))))
(reduction/context/name
"App" lang e
((t_0 t_1) s_0)
(term ((t_0 s_0) (t_1 s_0))))
(reduction/context/name
"Var" lang e
(number_0 s_0)
(term-let ((c_0 (list-ref (term s_0) (term number_0))))
(term c_0)))))
)