search

racket / redex

Other
93 stars 36 forks source link

Feature request: tag-with-names for apply-reduction-relation* #240

Closed xyzwwwww closed 3 years ago

xyzwwwww commented 3 years ago

Noticed that apply-reduction-relation* does not work with tag-with-names.

It can be useful for beginners and researchers to see the names of the reductions being applied when using apply-reduction-relation* with compatible closure and context-closure also maybe.

rfindler commented 3 years ago

I completely agree with the sentiment behind this request, but I think that taking this specific action would be tricky because there may be many ways to reach a particular irreducible term and indicating that in a simple way doesn't seem possible.

That said, it is thoughts like this that led me to build the redex/gui library. Did you try traces or stepper?

xyzwwwww commented 3 years ago

Yes, redex/GUI does the deed.

My main concern was that it requires me to build it.

But I see your point regarding the implementation. Thanks.