more control over normalization by expansion

[wilbowma]

This is also part of turnstile-core and non-critical.

Currently, evaluation happens during macro expansion. Essentially all evaluation, it seems. This is a problem for tooling (e.g., turnstile-drracket loses track of things since they no longer exist after expansion), and is against most intuition, and probably the semantics we want.

e.g., define actually produces a macro that inlines the definition everywhere, application expands to app/eval which attempts to perform the beta reduction during expansion, and similarly with elim.

A few syntax parameters should allow us more control, continue using this technique for conversion, but not perform all computation during expansion.

[stchang]

dupe of #37?

[wilbowma]

Yup