Hi Burke, That's great to hear that you're considering something like that. Like Neil, I'm in the "easy" position of stating a wish.
Neil's description is pretty much what I have in mind. (maybe drawing the derivation tree bottom-up instead of left-to-right, but that's a detail) -- Éric On Mar 7, 2012, at 7:37 PM, Neil Toronto wrote: > 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 > ____________________ Racket Users list: http://lists.racket-lang.org/users
