[racket] Redex: selective rendering of metafunctions/judgments

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Wed Aug 8 20:17:32 EDT 2012

Here's how it works for metafunctions.

#lang racket/base
(require redex/reduction-semantics redex/pict)
(define-language L)
(define-metafunction L
  [(f (any)) (f any)]
  [(f any) any])

(parameterize ([metafunction-cases '(1)])
  (render-metafunction f))


On Wed, Aug 8, 2012 at 5:19 PM, Asumu Takikawa <asumu at ccs.neu.edu> wrote:
> Hi all,
>
> I've found the `render-reduction-relation-rules` parameter for Redex
> typesetting very useful in the past for selectively rendering parts of a
> reduction relation.
>
> Is there any equivalent for metafunctions and judgment-forms? I couldn't
> find any in the docs. I imagine it's harder because clauses for these
> are not named, unlike reduction relations.
>
> Would it be possible to allow optional names for judgment clauses?
> Alternatively, even allowing selective rendering based on integer
> indices would be useful.
>
> Cheers,
> Asumu
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users

Posted on the users mailing list.