Implement redex-define

[shhyou]

This pull request implements a limited form of redex-define.

term is implemented using datum. Since there's no define/with-datum, I don't see an easy way to support variables with ellipses in redex-define. The current implementation of redex-define signals a syntax error upon encountering ellipses.

[wilbowma]

Could you say how this differs from define-term (https://docs.racket-lang.org/redex/The_Redex_Reference.html?q=define-term#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-term%29%29)?

Oh after a more careful reading of the examples, it looks like this allows multiple definitions by pattern matching, whereas define-term defines a single identifier. It would be worth pointing that out in the docs, perhaps, or maybe pointing define-term docs to this since it's strictly more general.

[shhyou]

Also, define-term does not perform pattern matching. It merely introduces a new binding.

[rfindler]

If there was a version of term-let that was based on define instead of let, would that be enough to support redex-define?

[shhyou]

Yes it would. That probably requires changes to term. Currently ellipses is handled using with-datum and datum.