I'd like this, myself. I wouldn't be creating it, so that's easy to say.
I imagine something that behaves like `traces' but shows derivation
trees instead of expressions, and creates multiple nodes only when a
judgment rule is nondeterministic.
Neil
On 03/07/2012 02:15 PM, Burke Fetscher wrote:
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
____________________
Racket Users list:
http://lists.racket-lang.org/users
____________________
Racket Users list:
http://lists.racket-lang.org/users
