[racket] Redex: selective rendering of metafunctions/judgments
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