[racket] [redex] traces for derivation trees

From: Burke Fetscher (bfetscher at gmail.com)
Date: Wed Mar 7 16:15:18 EST 2012

Hi Eric -

Unfortunately there isn't a 'traces' equivalent for 'define-judgment-form' right now.  However, as someone who is working on related things in Redex I have had similar thoughts and think it's a great idea, so hopefully we will add it at some point in the future.  And if you have any further ideas about what you would want something like this to look like please send them my way.

Burke

On Mar 7, 2012, at 1:16 PM, Eric Tanter wrote:

> Hi,
> 
> As I'm enjoying the new `define-judgment-form' in Redex, I started to dream about an equivalent of `traces' for `judgment-holds'. 
> 
> I'm going to try to use Redex in a course based on Pierce's TAPL, and once students see `traces' for reduction relations, they will be a bit disappointed by the text-based output for typing derivations that one can obtain by using `current-traced-metafunctions'.
> 
> Is there something like that already? if not, does it sound feasible?
> 
> Thanks,
> 
> -- Éric
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users



Posted on the users mailing list.