[racket] Typesetting with subscripts in Redex

From: Nada Amin (namin at alum.mit.edu)
Date: Sun Sep 9 18:25:29 EDT 2012


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)
   (['p (lambda (lws) (list (list-ref lws 2)))]
    ['n (lambda (lws) (list "-" (list-ref lws 2)))])

> (dummy-rewriters (lambda () (render-term dummy (p 1))))
> (dummy-rewriters (lambda () (render-term dummy (n 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

Thanks. Best regards,

Posted on the users mailing list.