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
