[racket] Typesetting with subscripts in Redex

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

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

Posted on the users mailing list.