[racket] Typesetting with subscripts in Redex
Hello,
Redex has been really useful in exploring examples in a calculus we're
developing. Now, I would like to use Redex's typesetting facility to
render these examples (to avoid introducing bugs when translating them
to TeX). For this, it would be great if I could specify that something
should be rendered as a subscript.
Here is a dummy example just to illustrate what I mean:
#lang racket
(require redex)
(define-language dummy
(e (p natural) (n natural)))
(define (dummy-rewriters thunk)
(with-compound-rewriters
(['p (lambda (lws) (list (list-ref lws 2)))]
['n (lambda (lws) (list "-" (list-ref lws 2)))])
(thunk)))
> (dummy-rewriters (lambda () (render-term dummy (p 1))))
1
> (dummy-rewriters (lambda () (render-term dummy (n 1))))
-1
Let's say, I'd like to render (n 1) as the equivalent of TeX $1_n$. Is
that possible? Incidentally, is there a better way to re-use compound
rewriters?
Thanks. Best regards,
~n